--- a/src/Doc/antiquote_setup.ML Sat May 22 21:52:13 2021 +0200
+++ b/src/Doc/antiquote_setup.ML Sat May 22 22:58:10 2021 +0200
@@ -33,94 +33,6 @@
| clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c);
-(* ML text *)
-
-local
-
-fun test_val (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read ");"
- | test_val (ml1, ml2) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read ");";
-
-fun test_op (ml1, ml2) = test_val (ML_Lex.read "op " @ ml1, ml2);
-
-fun test_type (ml1, []) = ML_Lex.read "val _ = NONE : (" @ ml1 @ ML_Lex.read ") option;"
- | test_type (ml1, ml2) =
- ML_Lex.read "val _ = [NONE : (" @ ml1 @ ML_Lex.read ") option, NONE : (" @
- ml2 @ ML_Lex.read ") option];";
-
-fun text_exn (ml1, []) = ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : exn);"
- | text_exn (ml1, ml2) =
- ML_Lex.read "fn _ => (" @ ml1 @ ML_Lex.read " : " @ ml2 @ ML_Lex.read " -> exn);";
-
-fun test_struct (ml, _) =
- ML_Lex.read "functor XXX() = struct structure XX = " @ ml @ ML_Lex.read " end;";
-
-fun test_functor (Antiquote.Text tok :: _, _) =
- ML_Lex.read "ML_Env.check_functor " @
- ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
- | test_functor _ = raise Fail "Bad ML functor specification";
-
-val is_name =
- ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident);
-
-fun is_ml_identifier ants =
- forall Antiquote.is_text ants andalso
- (case filter is_name (map (Antiquote.the_text "") ants) of
- toks as [_] => Symbol_Pos.is_identifier (Long_Name.base_name (ML_Lex.flatten toks))
- | _ => false);
-
-val parse_ml = Args.text_input -- Scan.optional (Args.colon |-- Args.text_input) Input.empty;
-val parse_type = Args.text_input -- Scan.optional (Args.$$$ "=" |-- Args.text_input) Input.empty;
-val parse_exn = Args.text_input -- Scan.optional (Args.$$$ "of" |-- Args.text_input) Input.empty;
-val parse_struct = Args.text_input >> rpair Input.empty;
-
-fun antiquotation_ml parse test kind show_kind binding index =
- Document_Output.antiquotation_raw binding (Scan.lift parse)
- (fn ctxt => fn (source1, source2) =>
- let
- val (ml1, ml2) = apply2 ML_Lex.read_source (source1, source2);
- val pos = Input.pos_of source1;
- val _ =
- ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (test (ml1, ml2))
- handle ERROR msg => error (msg ^ Position.here pos);
-
- val (txt1, txt2) = apply2 (#1 o Input.source_content) (source1, source2);
- val sep = if kind = "type" then "=" else if kind = "exception" then "of" else ":";
- val txt =
- if txt2 = "" then txt1
- else if sep = ":" andalso is_ml_identifier ml1 then txt1 ^ ": " ^ txt2
- else txt1 ^ " " ^ sep ^ " " ^ txt2;
-
- val main_text =
- Document_Output.verbatim ctxt
- (if kind = "" orelse not show_kind then txt else kind ^ " " ^ txt);
-
- val index_text =
- index |> Option.map (fn def =>
- let
- val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt;
- val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")";
- val txt' = Latex.block [Document_Output.verbatim ctxt' txt1, Latex.string kind'];
- val like = Document_Antiquotation.approx_content ctxt source1;
- in Latex.index_entry {items = [{text = txt', like = like}], def = def} end);
- in Latex.block (the_list index_text @ [main_text]) end);
-
-fun antiquotation_ml' parse test kind binding =
- antiquotation_ml parse test kind true binding (SOME true);
-
-in
-
-val _ =
- Theory.setup
- (antiquotation_ml' parse_ml test_val "" \<^binding>\<open>define_ML\<close> #>
- antiquotation_ml' parse_ml test_op "infix" \<^binding>\<open>define_ML_infix\<close> #>
- antiquotation_ml' parse_type test_type "type" \<^binding>\<open>define_ML_type\<close> #>
- antiquotation_ml' parse_exn text_exn "exception" \<^binding>\<open>define_ML_exception\<close> #>
- antiquotation_ml' parse_struct test_struct "structure" \<^binding>\<open>define_ML_structure\<close> #>
- antiquotation_ml' parse_struct test_functor "functor" \<^binding>\<open>define_ML_functor\<close>);
-
-end;
-
-
(* named theorems *)
val _ =