14 fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");" |
14 fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");" |
15 | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ ");"; |
15 | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ ");"; |
16 |
16 |
17 fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;" |
17 fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;" |
18 | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];"; |
18 | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];"; |
19 |
19 |
|
20 fun ml_exc (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);" |
|
21 | ml_exc (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);"; |
|
22 |
20 fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
23 fun ml_structure (txt, _) = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;" |
21 |
24 |
22 fun ml_functor _ = "val _ = ();"; (*no check!*) |
25 fun ml_functor _ = "val _ = ();"; (*no check!*) |
23 |
26 |
24 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
27 val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
26 fun index_ml kind ml src ctxt (txt1, txt2) = |
29 fun index_ml kind ml src ctxt (txt1, txt2) = |
27 let |
30 let |
28 val txt = if txt2 = "" then txt1 else |
31 val txt = if txt2 = "" then txt1 else |
29 if kind = "type" |
32 if kind = "type" |
30 then txt1 ^ " = " ^ txt2 |
33 then txt1 ^ " = " ^ txt2 |
31 else txt1 ^ ": " ^ txt2; |
34 else if kind = "exception" |
|
35 then txt1 ^ " of " ^ txt2 |
|
36 else txt1 ^ ": " ^ txt2; |
32 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
37 val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
|
38 val _ = writeln (ml (txt1, txt2)); |
33 val _ = ML_Context.use_mltext (ml (txt1, txt2)) false (SOME (Context.Proof ctxt)); |
39 val _ = ML_Context.use_mltext (ml (txt1, txt2)) false (SOME (Context.Proof ctxt)); |
34 in |
40 in |
35 "\\indexml" ^ kind ^ enclose "{" "}" |
41 "\\indexml" ^ kind ^ enclose "{" "}" |
36 (translate_string (fn "_" => "-" | ">" => "$>$" | c => c) txt1) ^ |
42 (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^ |
37 ((if ! O.source then str_of_source src else txt') |
43 ((if ! O.source then str_of_source src else txt') |
38 |> (if ! O.quotes then quote else I) |
44 |> (if ! O.quotes then quote else I) |
39 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
45 |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
40 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
46 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
41 end; |
47 end; |
49 in |
55 in |
50 |
56 |
51 val _ = O.add_commands |
57 val _ = O.add_commands |
52 [("index_ML", arguments (index_ml "" ml_val)), |
58 [("index_ML", arguments (index_ml "" ml_val)), |
53 ("index_ML_type", arguments (index_ml "type" ml_type)), |
59 ("index_ML_type", arguments (index_ml "type" ml_type)), |
|
60 ("index_ML_exc", arguments (index_ml "exception" ml_exc)), |
54 ("index_ML_structure", arguments (index_ml "structure" ml_structure)), |
61 ("index_ML_structure", arguments (index_ml "structure" ml_structure)), |
55 ("index_ML_functor", arguments (index_ml "functor" ml_functor)), |
62 ("index_ML_functor", arguments (index_ml "functor" ml_functor)), |
56 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim), |
63 ("ML_functor", O.args (Scan.lift Args.name) output_verbatim), |
57 ("verbatim", O.args (Scan.lift Args.name) output_verbatim), |
64 ("verbatim", O.args (Scan.lift Args.name) output_verbatim), |
58 ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file)))]; |
65 ("thy_file", O.args (Scan.lift Args.name) (O.output (K pretty_thy_file)))]; |