src/Pure/Thy/thy_output.ML
changeset 30573 49899f26fbd1
parent 30513 1796b8ea88aa
child 30588 05f81bbb2614
     1.1 --- a/src/Pure/Thy/thy_output.ML	Wed Mar 18 20:03:01 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Wed Mar 18 21:55:38 2009 +0100
     1.3 @@ -22,7 +22,7 @@
     1.4      ({state: Toplevel.state, source: Args.src, context: Proof.context} -> 'a -> string) -> unit
     1.5    datatype markup = Markup | MarkupEnv | Verbatim
     1.6    val modes: string list ref
     1.7 -  val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
     1.8 +  val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
     1.9    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    1.10      (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    1.11    val pretty_text: string -> Pretty.T
    1.12 @@ -156,7 +156,7 @@
    1.13            end
    1.14        | expand (Antiquote.Open _) = ""
    1.15        | expand (Antiquote.Close _) = "";
    1.16 -    val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
    1.17 +    val ants = Antiquote.read (Symbol_Pos.explode (txt, pos), pos);
    1.18    in
    1.19      if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
    1.20        error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
    1.21 @@ -577,7 +577,7 @@
    1.22  fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
    1.23    (fn {context, ...} => fn (txt, pos) =>
    1.24     (ML_Context.eval_in (SOME context) false pos (ml txt);
    1.25 -    SymbolPos.content (SymbolPos.explode (txt, pos))
    1.26 +    Symbol_Pos.content (Symbol_Pos.explode (txt, pos))
    1.27      |> (if ! quotes then quote else I)
    1.28      |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.29      else