diff -r e08c9f755fca -r f6a4da31f2f1 src/Tools/WWW_Find/find_theorems.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/WWW_Find/find_theorems.ML	Fri Nov 20 18:36:44 2009 +1100
@@ -0,0 +1,244 @@
+(*  Title:      find_theorems.ML
+    Author:     Timothy Bourke, NICTA
+
+    Simple find_theorems server
+*)
+
+local
+val default_limit = 20;
+val thy_names = sort string_ord (ThyInfo.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 (Int.toString 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;
+
+    fun prfxwith s = let
+        val (c, v) =
+          if b
+          then ("criterion", "with " ^ s)
+          else ("ncriterion", "without " ^ 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, query, args) =
+  let
+    val args =
+      (case othmslen of
+         NONE => args
+       | SOME l => Symtab.update ("limit", Int.toString l) args)
+    val qargs = HttpUtil.make_query_string args;
+
+    val num_found_text =
+      (case othmslen of
+         NONE => text (Int.toString thmslen)
+       | SOME l =>
+           a { href = find_theorems_url ^
+               (if qargs = "" then "" else "?" ^ qargs),
+           text = Int.toString l })
+    val found = [text "found ", num_found_text, text " theorems"] : tag list;
+    val displayed =
+      if is_some othmslen
+      then " (" ^ Int.toString thmslen ^ " displayed)"
+      else "";
+    fun show_search c = tr [ td' noid [show_criterion c] ];
+  in
+    table (class "findtheoremsquery")
+    (* [ tr [ th (noid, "searched for:") ] ]
+       @ map show_search query @ *)
+      [ 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 string_of_thm =
+      Output.output o Pretty.setmp_margin_CRITICAL 100 Pretty.string_of o
+        setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
+  in
+    tag' "tr" (class ("row" ^ Int.toString (n mod 2)))
+      [
+        tag' "td" (class "name")
+          [span' (sorry_class thm)
+             [raw_text (Facts.string_of_ref thmref)]
+          ],
+        tag' "td" (class "thm") [pre noid (string_of_thm thm)]
+      ]
+  end;
+
+end;
+
+structure P = OuterParse
+      and K = OuterKeyword
+      and FT = Find_Theorems;
+
+val criterion =
+  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Find_Theorems.Name ||
+  P.reserved "intro" >> K Find_Theorems.Intro ||
+  P.reserved "elim" >> K Find_Theorems.Elim ||
+  P.reserved "dest" >> K Find_Theorems.Dest ||
+  P.reserved "solves" >> K Find_Theorems.Solves ||
+  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Find_Theorems.Simp ||
+  P.term >> Find_Theorems.Pattern;
+
+val parse_query =
+  Scan.repeat (((Scan.option P.minus >> is_none) -- criterion));
+
+fun app_index f xs = fold_index (fn x => K (f x)) xs ();
+
+fun find_theorems (req as ScgiReq.Req {request_method, query_string, ...},
+                   content, send) =
+  let
+    val arg_data =
+      (case request_method of
+         ScgiReq.Get => query_string
+       | ScgiReq.Post =>
+          content
+          |> Byte.bytesToString
+          |> HttpUtil.parse_query_string
+       | ScgiReq.Head => raise Fail "Cannot handle Head requests.");
+
+    val args = Symtab.lookup arg_data;
+
+    val query = the_default "" (args "query");
+    fun get_query () =
+      query
+      |> (fn s => s ^ ";")
+      |> OuterSyntax.scan Position.start
+      |> filter OuterLex.is_proper
+      |> Scan.error parse_query
+      |> fst;
+
+    val limit =
+      args "limit"
+      |> Option.mapPartial Int.fromString
+      |> the_default default_limit;
+    val thy_name =
+      args "theory"
+      |> the_default "Main";
+    val with_dups = is_some (args "with_dups");
+
+    fun do_find () =
+      let
+        val ctxt = ProofContext.init (theory thy_name);
+        val query = get_query ();
+        val (othmslen, thms) = apsnd rev
+          (Find_Theorems.find_theorems ctxt NONE (SOME limit) with_dups query);
+        val thmslen = length thms;
+        fun thm_row args = Xhtml.write send (html_thm ctxt args);
+      in
+        Xhtml.write send
+          (find_theorems_summary (othmslen, thmslen, query, arg_data));
+        if null thms then ()
+        else (Xhtml.write_open send find_theorems_table;
+              HTML_Unicode.print_mode (app_index thm_row) thms;
+              Xhtml.write_close send find_theorems_table)
+      end;
+
+    val header = (html_header thy_name (args "query", limit, with_dups));
+  in
+    send Xhtml.doctype_xhtml1_0_strict;
+    Xhtml.write_open send header;
+    if query = "" then ()
+    else
+      do_find ()
+        handle
+          ERROR msg => Xhtml.write send (html_error msg)
+        | e => Xhtml.write send (html_error ("Server error: " ^ exnMessage e));
+    Xhtml.write_close send header
+  end;
+in
+val () = show_question_marks := false;
+val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
+end;
+