# HG changeset patch
# User krauss
# Date 1306768068 -7200
# Node ID a4c985fe015d8615153991e1666dc238d619924d
# Parent  8aeb7ec8003ab55fa4e93586657e0e1b7e6fe394
moved html templates to a separate module, making their awkward signatures explicit

diff -r 8aeb7ec8003a -r a4c985fe015d src/Tools/WWW_Find/IsaMakefile
--- a/src/Tools/WWW_Find/IsaMakefile	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/IsaMakefile	Mon May 30 17:07:48 2011 +0200
@@ -29,8 +29,8 @@
 	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
 
 $(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML \
-  http_status.ML http_util.ML mime.ML scgi_req.ML scgi_server.ML \
-  socket_util.ML unicode_symbols.ML xhtml.ML ROOT.ML
+  html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML \
+  scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML ROOT.ML
 	@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
 
 
diff -r 8aeb7ec8003a -r a4c985fe015d src/Tools/WWW_Find/ROOT.ML
--- a/src/Tools/WWW_Find/ROOT.ML	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/ROOT.ML	Mon May 30 17:07:48 2011 +0200
@@ -10,5 +10,6 @@
   use "scgi_req.ML";
   use "scgi_server.ML";
   use "echo.ML";
+  use "html_templates.ML";
   use "find_theorems.ML")
 else ()
diff -r 8aeb7ec8003a -r a4c985fe015d src/Tools/WWW_Find/find_theorems.ML
--- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
+++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
@@ -7,147 +7,7 @@
 local
 
 val default_limit = 20;
-val thy_names = sort string_ord (Thy_Info.get_names ());
-
-val find_theorems_url = "find_theorems";
-
-fun is_sorry thm =
-  Thm.proof_of thm
-  |> Proofterm.approximate_proof_body
-  |> Proofterm.all_oracles_of
-  |> exists (fn (x, _) => x = "Pure.skip_proof");
-
-local open Xhtml in
-fun find_theorems_form thy_name (query, limit, withdups) =
-  let
-    val query_input =
-      input (id "query", {
-        name = "query",
-        itype = TextInput { value = query, maxlength = NONE }});
-
-    val max_results = divele noid
-      [
-        label (noid, { for = "limit" }, "Max. results:"),
-        input (id "limit",
-          { name = "limit",
-            itype = TextInput { value = SOME (string_of_int limit),
-                                maxlength = NONE }})
-      ];
-
-    val theories = divele noid
-      [
-        label (noid, { for = "theory" }, "Search in:"),
-        select (id "theory", { name = "theory", value = SOME thy_name })
-               thy_names
-      ];
-
-    val with_dups = divele noid
-      [
-        label (noid, { for = "withdups" }, "Allow duplicates:"),
-        input (id "withdups",
-          { name = "withdups",
-            itype = Checkbox { checked = withdups, value = SOME "true" }})
-      ];
-
-    val help = divele (class "help")
-      [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
-  in
-    form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
-      [tag "fieldset" []
-        [tag "legend" [] [text "find_theorems"],
-         (add_script (OnKeyPress, "encodequery(this)")
-          o add_script (OnChange, "encodequery(this)")
-          o add_script (OnMouseUp, "encodequery(this)")) query_input,
-         divele (class "settings") [ max_results, theories, with_dups, help ],
-         divele (class "mainbuttons")
-           [ reset_button (id "reset"), submit_button (id "submit") ]
-        ]
-      ]
-  end;
-
-fun html_header thy_name args =
-  html { lang = "en" } [
-    head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
-         [script (noid, { script_type="text/javascript",
-                          src="/find_theorems.js" })],
-    add_script (OnLoad, "encodequery(document.getElementById('query'))")
-      (body noid [
-          h (noid, 1, "Theory " ^ thy_name),
-          find_theorems_form thy_name args,
-          divele noid []
-         ])
-  ];
-
-fun html_error msg = p ((class "error"), msg);
-
-val find_theorems_table =
-  table (class "findtheorems")
-    [
-      thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
-      tbody noid []
-    ];
-
-fun show_criterion (b, c) =
-  let
-    fun prfx s = let
-        val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
-      in span (class c, v) end;
-  in
-    (case c of
-      Find_Theorems.Name name => prfx ("name: " ^ quote name)
-    | Find_Theorems.Intro => prfx "intro"
-    | Find_Theorems.IntroIff => prfx "introiff"
-    | Find_Theorems.Elim => prfx "elim"
-    | Find_Theorems.Dest => prfx "dest"
-    | Find_Theorems.Solves => prfx "solves"
-    | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
-    | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
-  end;
-
-fun find_theorems_summary (othmslen, thmslen, args) =
-  let
-    val args =
-      (case othmslen of
-         NONE => args
-       | SOME l => Symtab.update ("limit", string_of_int l) args)
-    val qargs = HttpUtil.make_query_string args;
-
-    val num_found_text =
-      (case othmslen of
-         NONE => text (string_of_int thmslen)
-       | SOME l =>
-           a { href = find_theorems_url ^
-               (if qargs = "" then "" else "?" ^ qargs),
-           text = string_of_int l })
-    val found = [text "found ", num_found_text, text " theorems"] : tag list;
-    val displayed =
-      if is_some othmslen
-      then " (" ^ string_of_int thmslen ^ " displayed)"
-      else "";
-  in
-    table (class "findtheoremsquery")
-      [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
-  end
-
-fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
-
-fun html_thm ctxt (n, (thmref, thm)) =
-  let
-    val output_thm =
-      Output.output o Pretty.string_of_margin 100 o
-        Display.pretty_thm (Config.put show_question_marks false ctxt);
-  in
-    tag' "tr" (class ("row" ^ string_of_int (n mod 2)))
-      [
-        tag' "td" (class "name")
-          [span' (sorry_class thm)
-             [raw_text (Facts.string_of_ref thmref)]
-          ],
-        tag' "td" (class "thm") [pre noid (output_thm thm)]
-      ]
-  end;
-
-end;
+val all_thy_names = sort string_ord (Thy_Info.get_names ());
 
 fun app_index f xs = fold_index (fn x => K (f x)) xs ();
 
@@ -188,25 +48,25 @@
           ||> rev;
       in
         Xhtml.write send
-          (find_theorems_summary (othmslen, length thms, arg_data));
+          (HTML_Templates.find_theorems_summary (othmslen, length thms, arg_data));
         if null thms then ()
-        else Xhtml.write_enclosed send find_theorems_table (fn send =>
-               HTML_Unicode.print_mode (app_index (Xhtml.write send o html_thm ctxt)) thms)
+        else Xhtml.write_enclosed send HTML_Templates.find_theorems_table (fn send =>
+               HTML_Unicode.print_mode (app_index (Xhtml.write send o HTML_Templates.html_thm ctxt)) thms)
       end;
   in
     send Xhtml.doctype_xhtml1_0_strict;
     Xhtml.write_enclosed send
-      (html_header thy_name (args "query", limit, with_dups))
+      (HTML_Templates.header thy_name (args "query", limit, with_dups, all_thy_names))
       (fn send => 
         if query_str = "" then ()
         else
           do_find (get_query ())
-          handle ERROR msg => Xhtml.write send (html_error msg))
+          handle ERROR msg => Xhtml.write send (HTML_Templates.error msg))
   end;
 in
 
 val () = Printer.show_question_marks_default := false;
-val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems o parse_request);
+val () = ScgiServer.register ("find_theorems", SOME Mime.html, find_theorems o parse_request);
 
 end;
 
diff -r 8aeb7ec8003a -r a4c985fe015d src/Tools/WWW_Find/html_templates.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/html_templates.ML	Mon May 30 17:07:48 2011 +0200
@@ -0,0 +1,163 @@
+(*  Title:      Tools/WWW_Find/html_templates.ML
+    Author:     Timothy Bourke, NICTA
+
+HTML Templates for find theorems server.
+*)
+
+signature HTML_TEMPLATES =
+sig
+  val find_theorems_form: string -> (string option * int * bool * string list) -> Xhtml.tag
+
+  val header: string -> (string option * int * bool * string list) -> Xhtml.tag
+  val error: string -> Xhtml.tag
+  val find_theorems_table: Xhtml.tag
+
+  val find_theorems_summary: int option * int * string Symtab.table -> Xhtml.tag
+  val html_thm: Proof.context -> (int * (Facts.ref * thm)) -> Xhtml.tag
+end
+
+
+structure HTML_Templates: HTML_TEMPLATES =
+struct
+
+open Xhtml;
+
+fun find_theorems_form thy_name (query, limit, withdups, all_thy_names) =
+  let
+    val query_input =
+      input (id "query", {
+        name = "query",
+        itype = TextInput { value = query, maxlength = NONE }});
+
+    val max_results = divele noid
+      [
+        label (noid, { for = "limit" }, "Max. results:"),
+        input (id "limit",
+          { name = "limit",
+            itype = TextInput { value = SOME (string_of_int limit),
+                                maxlength = NONE }})
+      ];
+
+    val theories = divele noid
+      [
+        label (noid, { for = "theory" }, "Search in:"),
+        select (id "theory", { name = "theory", value = SOME thy_name })
+               all_thy_names
+      ];
+
+    val with_dups = divele noid
+      [
+        label (noid, { for = "withdups" }, "Allow duplicates:"),
+        input (id "withdups",
+          { name = "withdups",
+            itype = Checkbox { checked = withdups, value = SOME "true" }})
+      ];
+
+    val help = divele (class "help")
+      [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
+  in
+    form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
+      [tag "fieldset" []
+        [tag "legend" [] [text "find_theorems"],
+         (add_script (OnKeyPress, "encodequery(this)")
+          o add_script (OnChange, "encodequery(this)")
+          o add_script (OnMouseUp, "encodequery(this)")) query_input,
+         divele (class "settings") [ max_results, theories, with_dups, help ],
+         divele (class "mainbuttons")
+           [ reset_button (id "reset"), submit_button (id "submit") ]
+        ]
+      ]
+  end;
+
+fun header thy_name args =
+  html { lang = "en" } [
+    head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
+         [script (noid, { script_type="text/javascript",
+                          src="/find_theorems.js" })],
+    add_script (OnLoad, "encodequery(document.getElementById('query'))")
+      (body noid [
+          h (noid, 1, "Theory " ^ thy_name),
+          find_theorems_form thy_name args,
+          divele noid []
+         ])
+  ];
+
+fun error msg = p ((class "error"), msg);
+
+val find_theorems_table =
+  table (class "findtheorems")
+    [
+      thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
+      tbody noid []
+    ];
+
+fun show_criterion (b, c) =
+  let
+    fun prfx s = let
+        val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
+      in span (class c, v) end;
+  in
+    (case c of
+      Find_Theorems.Name name => prfx ("name: " ^ quote name)
+    | Find_Theorems.Intro => prfx "intro"
+    | Find_Theorems.IntroIff => prfx "introiff"
+    | Find_Theorems.Elim => prfx "elim"
+    | Find_Theorems.Dest => prfx "dest"
+    | Find_Theorems.Solves => prfx "solves"
+    | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
+    | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
+  end;
+
+fun find_theorems_summary (othmslen, thmslen, args) =
+  let
+    val args =
+      (case othmslen of
+         NONE => args
+       | SOME l => Symtab.update ("limit", string_of_int l) args)
+    val qargs = HttpUtil.make_query_string args;
+
+    val num_found_text =
+      (case othmslen of
+         NONE => text (string_of_int thmslen)
+       | SOME l =>
+           a { href = "find_theorems" ^
+               (if qargs = "" then "" else "?" ^ qargs),
+           text = string_of_int l })
+    val found = [text "found ", num_found_text, text " theorems"] : tag list;
+    val displayed =
+      if is_some othmslen
+      then " (" ^ string_of_int thmslen ^ " displayed)"
+      else "";
+  in
+    table (class "findtheoremsquery")
+      [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
+  end
+
+(*FIXME!?!*)
+fun is_sorry thm =
+  Thm.proof_of thm
+  |> Proofterm.approximate_proof_body
+  |> Proofterm.all_oracles_of
+  |> exists (fn (x, _) => x = "Pure.skip_proof");
+
+fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
+
+fun html_thm ctxt (n, (thmref, thm)) =
+  let
+    val output_thm =
+      Output.output o Pretty.string_of_margin 100 o
+        Display.pretty_thm (Config.put show_question_marks false ctxt);
+  in
+    tag' "tr" (class ("row" ^ string_of_int (n mod 2)))
+      [
+        tag' "td" (class "name")
+          [span' (sorry_class thm)
+             [raw_text (Facts.string_of_ref thmref)]
+          ],
+        tag' "td" (class "thm") [pre noid (output_thm thm)]
+      ]
+  end;
+
+end;
+
+