ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;
authorwenzelm
Tue Mar 03 12:12:38 2009 +0100 (2009-03-03)
changeset 302080abadde7b3fb
parent 30205 e33ce8d765b4
child 30209 9e245d524997
ignore "source" option in antiquotations @{ML}, @{ML_type}, @{ML_struct} -- did not really make sense, without it users can enable source mode globally with less surprises;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Mar 02 20:31:27 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Mar 03 12:12:38 2009 +0100
     1.3 @@ -519,9 +519,9 @@
     1.4  fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
     1.5  fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
     1.6  
     1.7 -fun output_ml ml src ctxt (txt, pos) =
     1.8 +fun output_ml ml _ ctxt (txt, pos) =
     1.9   (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
    1.10 -  (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
    1.11 +  SymbolPos.content (SymbolPos.explode (txt, pos))
    1.12    |> (if ! quotes then quote else I)
    1.13    |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.14    else