src/Pure/Thy/thy_output.ML
changeset 27874 f0364f1c0ecf
parent 27809 a1e409db516b
child 27882 eaa9fef9f4c1
     1.1 --- a/src/Pure/Thy/thy_output.ML	Thu Aug 14 19:52:39 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Aug 14 19:52:40 2008 +0200
     1.3 @@ -22,7 +22,7 @@
     1.4      (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.node option -> string
     1.5    datatype markup = Markup | MarkupEnv | Verbatim
     1.6    val modes: string list ref
     1.7 -  val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string
     1.8 +  val eval_antiquote: Scan.lexicon -> Toplevel.node option -> SymbolPos.text * Position.T -> string
     1.9    val process_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    1.10      Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    1.11    val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
    1.12 @@ -145,7 +145,7 @@
    1.13  
    1.14  val modes = ref ([]: string list);
    1.15  
    1.16 -fun eval_antiquote lex node (str, pos) =
    1.17 +fun eval_antiquote lex node (txt, pos) =
    1.18    let
    1.19      fun expand (Antiquote.Text s) = s
    1.20        | expand (Antiquote.Antiq x) =
    1.21 @@ -156,7 +156,7 @@
    1.22            end
    1.23        | expand (Antiquote.Open _) = ""
    1.24        | expand (Antiquote.Close _) = "";
    1.25 -    val ants = Antiquote.read (str, pos);
    1.26 +    val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
    1.27    in
    1.28      if is_none node andalso exists Antiquote.is_antiq ants then
    1.29        error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)
    1.30 @@ -334,7 +334,7 @@
    1.31      fun markup mark mk flag = Scan.peek (fn d =>
    1.32        improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
    1.33        Scan.repeat tag --
    1.34 -      P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
    1.35 +      P.!!!! ((improper -- locale -- improper) |-- P.doc_source --| improper_end)
    1.36        >> (fn (((tok, pos), tags), txt) =>
    1.37          let val name = T.content_of tok
    1.38          in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
    1.39 @@ -347,7 +347,7 @@
    1.40          in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
    1.41  
    1.42      val cmt = Scan.peek (fn d =>
    1.43 -      P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text)
    1.44 +      P.$$$ "--" |-- P.!!!! (improper |-- P.doc_source)
    1.45        >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
    1.46  
    1.47      val other = Scan.peek (fn d =>