src/Pure/Thy/html.ML
changeset 59448 149d2bc5ddb6
parent 55041 368ee97e03ce
child 61374 b3c665940d62
     1.1 --- a/src/Pure/Thy/html.ML	Mon Jan 26 13:44:37 2015 +0100
     1.2 +++ b/src/Pure/Thy/html.ML	Mon Jan 26 13:48:29 2015 +0100
     1.3 @@ -20,8 +20,7 @@
     1.4    val verbatim: string -> text
     1.5    val begin_document: string -> text
     1.6    val end_document: text
     1.7 -  val begin_session_index: string -> (Url.T * string) list -> Url.T -> text
     1.8 -  val applet_pages: string -> Url.T * string -> (string * string) list
     1.9 +  val begin_session_index: string -> Url.T -> (Url.T * string) list -> text
    1.10    val theory_entry: Url.T * string -> text
    1.11    val theory: string -> (Url.T option * string) list -> text -> text
    1.12  end;
    1.13 @@ -280,42 +279,12 @@
    1.14  
    1.15  (* session index *)
    1.16  
    1.17 -fun begin_session_index session docs graph =
    1.18 +fun begin_session_index session graph docs =
    1.19    begin_document ("Session " ^ plain session) ^
    1.20    para ("View " ^ href_path graph "theory dependencies" ^
    1.21      implode (map (fn (p, name) => "<br/>\nView " ^ href_path p name) docs)) ^
    1.22    "\n</div>\n<div class=\"theories\">\n<h2>Theories</h2>\n<ul>\n";
    1.23  
    1.24 -fun choice chs s = space_implode " " (map (fn (s', lnk) =>
    1.25 -  enclose "[" "]" (if s = s' then keyword s' else href_name lnk s')) chs);
    1.26 -
    1.27 -fun back_link (path, name) = para (href_path path "Back" ^ " to index of " ^ plain name);
    1.28 -
    1.29 -fun applet_pages session back =
    1.30 -  let
    1.31 -    val sizes =
    1.32 -     [("small", "small.html", ("500", "400")),
    1.33 -      ("medium", "medium.html", ("650", "520")),
    1.34 -      ("large", "large.html", ("800", "640"))];
    1.35 -
    1.36 -    fun applet_page (size, name, (width, height)) =
    1.37 -      let
    1.38 -        val browser_size = "Set browser size: " ^
    1.39 -          choice (map (fn (y, z, _) => (y, z)) sizes) size;
    1.40 -      in
    1.41 -        (name, begin_document ("Theory dependencies of " ^ session) ^
    1.42 -          back_link back ^
    1.43 -          para browser_size ^
    1.44 -          "\n</div>\n<div class=\"graphbrowser\">\n\
    1.45 -          \<applet code=\"GraphBrowser/GraphBrowser.class\" \
    1.46 -          \archive=\"GraphBrowser.jar\" \
    1.47 -          \width=" ^ quote width ^ " height=" ^ quote height ^ ">\n\
    1.48 -          \<param name=\"graphfile\" value=\"" ^ "session.graph" ^ "\"/>\n\
    1.49 -          \</applet>" ^ end_document)
    1.50 -      end;
    1.51 -  in map applet_page sizes end;
    1.52 -
    1.53 -
    1.54  fun theory_entry (p, s) = "<li>" ^ href_path p (plain s) ^ "</li>\n";
    1.55  
    1.56