src/Tools/WWW_Find/html_templates.ML
author blanchet
Mon, 26 Nov 2012 13:35:05 +0100
changeset 50222 40e3c3be6bca
parent 46719 61cd0ad6cd42
permissions -rw-r--r--
added file headers
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
     1
(*  Title:      Tools/WWW_Find/html_templates.ML
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
     2
    Author:     Timothy Bourke, NICTA
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
     3
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
     4
HTML Templates for find theorems server.
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
     5
*)
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
     6
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
     7
signature HTML_TEMPLATES =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
     8
sig
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
     9
  val find_theorems_form: string -> (string option * int * bool * string list) -> Xhtml.tag
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    10
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    11
  val header: string -> (string option * int * bool * string list) -> Xhtml.tag
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    12
  val error: string -> Xhtml.tag
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    13
  val find_theorems_table: Xhtml.tag
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    14
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    15
  val find_theorems_summary: int option * int * string Symtab.table -> Xhtml.tag
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    16
  val html_thm: Proof.context -> (int * (Facts.ref * thm)) -> Xhtml.tag
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    17
end
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    18
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    19
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    20
structure HTML_Templates: HTML_TEMPLATES =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    21
struct
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    22
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    23
open Xhtml;
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    24
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    25
fun find_theorems_form thy_name (query, limit, withdups, all_thy_names) =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    26
  let
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    27
    val query_input =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    28
      input (id "query", {
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    29
        name = "query",
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    30
        itype = TextInput { value = query, maxlength = NONE }});
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    31
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    32
    val max_results = divele noid
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    33
      [
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    34
        label (noid, { for = "limit" }, "Max. results:"),
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    35
        input (id "limit",
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    36
          { name = "limit",
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    37
            itype = TextInput { value = SOME (string_of_int limit),
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    38
                                maxlength = NONE }})
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    39
      ];
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    40
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    41
    val theories = divele noid
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    42
      [
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    43
        label (noid, { for = "theory" }, "Search in:"),
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    44
        select (id "theory", { name = "theory", value = SOME thy_name })
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    45
               all_thy_names
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    46
      ];
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    47
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    48
    val with_dups = divele noid
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    49
      [
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    50
        label (noid, { for = "withdups" }, "Allow duplicates:"),
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    51
        input (id "withdups",
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    52
          { name = "withdups",
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    53
            itype = Checkbox { checked = withdups, value = SOME "true" }})
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    54
      ];
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    55
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    56
    val help = divele (class "help")
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    57
      [ a { href="/pasting_help.html", text="(pasting from proof general)" } ];
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    58
  in
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    59
    form (id "findtheorems", { method = "post", action = "/isabelle/find_theorems" })
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    60
      [tag "fieldset" []
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    61
        [tag "legend" [] [text "find_theorems"],
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    62
         (add_script (OnKeyPress, "encodequery(this)")
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    63
          o add_script (OnChange, "encodequery(this)")
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    64
          o add_script (OnMouseUp, "encodequery(this)")) query_input,
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    65
         divele (class "settings") [ max_results, theories, with_dups, help ],
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    66
         divele (class "mainbuttons")
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    67
           [ reset_button (id "reset"), submit_button (id "submit") ]
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    68
        ]
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    69
      ]
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    70
  end;
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    71
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    72
fun header thy_name args =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    73
  html { lang = "en" } [
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    74
    head { title = "Find Theorems: results", stylesheet_href = "/basic.css" }
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    75
         [script (noid, { script_type="text/javascript",
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    76
                          src="/find_theorems.js" })],
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    77
    add_script (OnLoad, "encodequery(document.getElementById('query'))")
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    78
      (body noid [
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    79
          h (noid, 1, "Theory " ^ thy_name),
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    80
          find_theorems_form thy_name args,
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    81
          divele noid []
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    82
         ])
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    83
  ];
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    84
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    85
fun error msg = p ((class "error"), msg);
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    86
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    87
val find_theorems_table =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    88
  table (class "findtheorems")
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    89
    [
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    90
      thead noid [tr [th (noid, "name"), th (noid, "theorem")]],
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    91
      tbody noid []
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    92
    ];
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    93
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    94
fun show_criterion (b, c) =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    95
  let
46719
61cd0ad6cd42 removed introiff (cf. b09afce1e54f);
wenzelm
parents: 43073
diff changeset
    96
    fun prfx s =
61cd0ad6cd42 removed introiff (cf. b09afce1e54f);
wenzelm
parents: 43073
diff changeset
    97
      let
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    98
        val (c, v) = if b then ("criterion", s) else ("ncriterion", "-" ^ s);
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
    99
      in span (class c, v) end;
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   100
  in
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   101
    (case c of
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   102
      Find_Theorems.Name name => prfx ("name: " ^ quote name)
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   103
    | Find_Theorems.Intro => prfx "intro"
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   104
    | Find_Theorems.Elim => prfx "elim"
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   105
    | Find_Theorems.Dest => prfx "dest"
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   106
    | Find_Theorems.Solves => prfx "solves"
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   107
    | Find_Theorems.Simp pat => prfx ("simp: \"" ^ pat ^ "\"")
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   108
    | Find_Theorems.Pattern pat => prfx ("\"" ^ pat ^ "\""))
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   109
  end;
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   110
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   111
fun find_theorems_summary (othmslen, thmslen, args) =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   112
  let
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   113
    val args =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   114
      (case othmslen of
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   115
         NONE => args
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   116
       | SOME l => Symtab.update ("limit", string_of_int l) args)
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   117
    val qargs = HttpUtil.make_query_string args;
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   118
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   119
    val num_found_text =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   120
      (case othmslen of
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   121
         NONE => text (string_of_int thmslen)
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   122
       | SOME l =>
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   123
           a { href = "find_theorems" ^
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   124
               (if qargs = "" then "" else "?" ^ qargs),
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   125
           text = string_of_int l })
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   126
    val found = [text "found ", num_found_text, text " theorems"] : tag list;
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   127
    val displayed =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   128
      if is_some othmslen
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   129
      then " (" ^ string_of_int thmslen ^ " displayed)"
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   130
      else "";
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   131
  in
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   132
    table (class "findtheoremsquery")
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   133
      [ tr [ th' noid (found @ [text (displayed ^ ":")]) ] ]
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   134
  end
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   135
46719
61cd0ad6cd42 removed introiff (cf. b09afce1e54f);
wenzelm
parents: 43073
diff changeset
   136
(* FIXME!?! *)
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   137
fun is_sorry thm =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   138
  Thm.proof_of thm
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   139
  |> Proofterm.approximate_proof_body
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   140
  |> Proofterm.all_oracles_of
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   141
  |> exists (fn (x, _) => x = "Pure.skip_proof");
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   142
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   143
fun sorry_class thm = if is_sorry thm then class "sorried" else noid;
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   144
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   145
fun html_thm ctxt (n, (thmref, thm)) =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   146
  let
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   147
    val output_thm =
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   148
      Output.output o Pretty.string_of_margin 100 o
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   149
        Display.pretty_thm (Config.put show_question_marks false ctxt);
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   150
  in
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   151
    tag' "tr" (class ("row" ^ string_of_int (n mod 2)))
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   152
      [
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   153
        tag' "td" (class "name")
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   154
          [span' (sorry_class thm)
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   155
             [raw_text (Facts.string_of_ref thmref)]
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   156
          ],
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   157
        tag' "td" (class "thm") [pre noid (output_thm thm)]
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   158
      ]
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   159
  end;
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   160
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   161
end;
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   162
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
diff changeset
   163