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;