1.1 --- a/src/Doc/antiquote_setup.ML Sat Mar 01 23:48:55 2014 +0100
1.2 +++ b/src/Doc/antiquote_setup.ML Sun Mar 02 00:05:35 2014 +0100
1.3 @@ -51,21 +51,29 @@
1.4
1.5 local
1.6
1.7 -fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");"
1.8 - | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ ");";
1.9 +val ml_toks = ML_Lex.read Position.none;
1.10
1.11 -fun ml_op (txt1, "") = "fn _ => (op " ^ txt1 ^ ");"
1.12 - | ml_op (txt1, txt2) = "fn _ => (op " ^ txt1 ^ " : " ^ txt2 ^ ");";
1.13 +fun ml_val (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks ");"
1.14 + | ml_val (toks1, toks2) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
1.15 +
1.16 +fun ml_op (toks1, []) = ml_toks "fn _ => (op " @ toks1 @ ml_toks ");"
1.17 + | ml_op (toks1, toks2) = ml_toks "fn _ => (op " @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
1.18
1.19 -fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;"
1.20 - | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];";
1.21 +fun ml_type (toks1, []) = ml_toks "val _ = NONE : (" @ toks1 @ ml_toks ") option;"
1.22 + | ml_type (toks1, toks2) =
1.23 + ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
1.24 + toks2 @ ml_toks ") option];";
1.25
1.26 -fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ " : exn);"
1.27 - | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ " -> exn);";
1.28 +fun ml_exn (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
1.29 + | ml_exn (toks1, toks2) =
1.30 + ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
1.31
1.32 -fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;";
1.33 +fun ml_structure (toks, _) =
1.34 + ml_toks "functor XXX() = struct structure XX = " @ toks @ ml_toks " end;";
1.35
1.36 -fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt;
1.37 +fun ml_functor (Antiquote.Text tok :: _, _) =
1.38 + ml_toks "ML_Env.check_functor " @ ml_toks (ML_Syntax.print_string (ML_Lex.content_of tok))
1.39 + | ml_functor _ = raise Fail "Bad ML functor specification";
1.40
1.41 val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent);
1.42
1.43 @@ -74,10 +82,19 @@
1.44 toks as [_] => ML_Lex.flatten toks
1.45 | _ => error ("Single ML name expected in input: " ^ quote txt));
1.46
1.47 +fun prep_ml source =
1.48 + (#1 (Symbol_Pos.source_content source), ML_Lex.read_source source);
1.49 +
1.50 fun index_ml name kind ml = Thy_Output.antiquotation name
1.51 - (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
1.52 - (fn {context = ctxt, ...} => fn (txt1, txt2) =>
1.53 + (Scan.lift (Args.name_source_position -- Scan.option (Args.colon |-- Args.name_source_position)))
1.54 + (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
1.55 let
1.56 + val (txt1, toks1) = prep_ml source1;
1.57 + val (txt2, toks2) =
1.58 + (case opt_source2 of
1.59 + SOME source => prep_ml source
1.60 + | NONE => ("", []));
1.61 +
1.62 val txt =
1.63 if txt2 = "" then txt1
1.64 else if kind = "type" then txt1 ^ " = " ^ txt2
1.65 @@ -86,15 +103,15 @@
1.66 then txt1 ^ ": " ^ txt2
1.67 else txt1 ^ " : " ^ txt2;
1.68 val txt' = if kind = "" then txt else kind ^ " " ^ txt;
1.69 - val _ = (* ML_Lex.read (!?) *)
1.70 - ML_Context.eval_source_in (SOME ctxt) false
1.71 - {delimited = false, text = ml (txt1, txt2), pos = Position.none};
1.72 +
1.73 + val _ = ML_Context.eval_in (SOME ctxt) false (#pos source1) (ml (toks1, toks2));
1.74 val kind' = if kind = "" then "ML" else "ML " ^ kind;
1.75 in
1.76 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
1.77 (txt'
1.78 |> (if Config.get ctxt Thy_Output.quotes then quote else I)
1.79 - |> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.80 + |> (if Config.get ctxt Thy_Output.display
1.81 + then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
1.82 else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
1.83 end);
1.84
1.85 @@ -105,7 +122,7 @@
1.86 index_ml @{binding index_ML_op} "infix" ml_op #>
1.87 index_ml @{binding index_ML_type} "type" ml_type #>
1.88 index_ml @{binding index_ML_exn} "exception" ml_exn #>
1.89 - index_ml @{binding index_ML_structure} "structure" ml_structure #>
1.90 + index_ml @{binding index_ML_struct} "structure" ml_structure #>
1.91 index_ml @{binding index_ML_functor} "functor" ml_functor;
1.92
1.93 end;