1.1 --- a/src/Pure/Thy/thy_output.ML	Sun May 30 18:23:50 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sun May 30 21:34:19 2010 +0200
     1.3 @@ -587,7 +587,7 @@
     1.4  
     1.5  fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
     1.6    (fn {context, ...} => fn (txt, pos) =>
     1.7 -   (ML_Context.eval_in (SOME context) false pos (ml txt);
     1.8 +   (ML_Context.eval_in (SOME context) false pos (ml pos txt);
     1.9      Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
    1.10      |> (if ! quotes then quote else I)
    1.11      |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.12 @@ -596,13 +596,21 @@
    1.13        #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|")
    1.14        #> space_implode "\\isasep\\isanewline%\n")));
    1.15  
    1.16 +fun ml_enclose bg en pos txt =
    1.17 +  ML_Lex.read Position.none bg @ ML_Lex.read pos txt @ ML_Lex.read Position.none en;
    1.18 +
    1.19  in
    1.20  
    1.21 -val _ = ml_text "ML" (fn txt => "fn _ => (" ^ txt ^ ");");
    1.22 -val _ = ml_text "ML_type" (fn txt => "val _ = NONE : (" ^ txt ^ ") option;");
    1.23 -val _ = ml_text "ML_struct" (fn txt => "functor XXX() = struct structure XX = " ^ txt ^ " end;");
    1.24 -val _ = ml_text "ML_functor" (fn txt => "ML_Env.check_functor " ^ ML_Syntax.print_string txt);
    1.25 -val _ = ml_text "ML_text" (K "");
    1.26 +val _ = ml_text "ML" (ml_enclose "fn _ => (" ");");
    1.27 +val _ = ml_text "ML_type" (ml_enclose "val _ = NONE : (" ") option;");
    1.28 +val _ = ml_text "ML_struct" (ml_enclose "functor XXX() = struct structure XX = " " end;");
    1.29 +
    1.30 +val _ = ml_text "ML_functor"   (* FIXME formal treatment of functor name (!?) *)
    1.31 +  (fn pos => fn txt =>
    1.32 +    ML_Lex.read Position.none ("ML_Env.check_functor " ^
    1.33 +      ML_Syntax.print_string (Symbol_Pos.content (Symbol_Pos.explode (txt, pos)))));
    1.34 +
    1.35 +val _ = ml_text "ML_text" (K (K []));
    1.36  
    1.37  end;
    1.38