Skip to content
Success

Changes

Summary

  1. merged
  2. pretty-printing sledgehammer command: merge indexed theorems
  3. clarify routes: absolute in api and relative for frontend;
  4. add auto-reload for more interactive web apps;
  5. clarified web app endpoints;
  6. proper html script tag: source code must not be escaped;
  7. add explicit Content-Length header to http response (otherwise it is missing in HEAD responses);
  8. add HEAD to http server: should send same header fields as if request was GET;
Changeset 80208:0604d3051eee by nipkow:
merged
Changeset 80207:ca7e7e41374e by nipkow:
pretty-printing sledgehammer command: merge indexed theorems
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML (diff)
Changeset 80206:3cf3ad092e3e by fabian huch _huch@in.tum.de_:
clarify routes: absolute in api and relative for frontend;
The file was modified src/Pure/System/web_app.scala (diff)
Changeset 80205:fc2d791d28bd by fabian huch _huch@in.tum.de_:
add auto-reload for more interactive web apps;
The file was modified src/Pure/System/web_app.scala (diff)
Changeset 80204:81f2fbf3975d by fabian huch _huch@in.tum.de_:
clarified web app endpoints;
The file was modified src/Pure/System/web_app.scala (diff)
Changeset 80203:ca9a402735b4 by fabian huch _huch@in.tum.de_:
proper html script tag: source code must not be escaped;
The file was modified src/Pure/General/html.scala (diff)
Changeset 80202:03c058592c58 by fabian huch _huch@in.tum.de_:
add explicit Content-Length header to http response (otherwise it is missing in HEAD responses);
The file was modified src/Pure/General/http.scala (diff)
Changeset 80201:6ac48d53d371 by fabian huch _huch@in.tum.de_:
add HEAD to http server: should send same header fields as if request was GET;
The file was modified src/Pure/General/http.scala (diff)