--- a/src/Pure/Thy/thy_output.ML Wed Mar 18 20:03:01 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Wed Mar 18 21:55:38 2009 +0100
@@ -22,7 +22,7 @@
({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
datatype markup = Markup | MarkupEnv | Verbatim
val modes: string list ref
- val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
+ val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
val pretty_text: string -> Pretty.T
@@ -156,7 +156,7 @@
end
| expand (Antiquote.Open _) = ""
| expand (Antiquote.Close _) = "";
- val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
+ val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
in
if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
@@ -577,7 +577,7 @@
fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
(fn {context, ...} => fn (txt, pos) =>
(ML_Context.eval_in (SOME context) false pos (ml txt);
- SymbolPos.content (SymbolPos.explode (txt, pos))
+ Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
|> (if ! quotes then quote else I)
|> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
else