antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
authorwenzelm
Thu Aug 14 19:52:40 2008 +0200 (2008-08-14)
changeset 27874f0364f1c0ecf
parent 27873 34d61938e27a
child 27875 1b46d9ec3788
antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
src/Pure/ML/ml_context.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/ML/ml_context.ML	Thu Aug 14 19:52:39 2008 +0200
     1.2 +++ b/src/Pure/ML/ml_context.ML	Thu Aug 14 19:52:40 2008 +0200
     1.3 @@ -124,9 +124,11 @@
     1.4  
     1.5  fun eval_antiquotes struct_name (txt, pos) opt_ctxt =
     1.6    let
     1.7 -    val ants = Antiquote.read (txt, pos);
     1.8 +    val syms = SymbolPos.explode (txt, pos);
     1.9 +    val ants = Antiquote.read (syms, pos);
    1.10      val ((ml_env, ml_body), opt_ctxt') =
    1.11 -      if not (exists Antiquote.is_antiq ants) then (("", Symbol.escape txt), opt_ctxt)
    1.12 +      if not (exists Antiquote.is_antiq ants)
    1.13 +      then (("", Symbol.escape (SymbolPos.content syms)), opt_ctxt)
    1.14        else
    1.15          let
    1.16            val ctxt =
     2.1 --- a/src/Pure/Thy/latex.ML	Thu Aug 14 19:52:39 2008 +0200
     2.2 +++ b/src/Pure/Thy/latex.ML	Thu Aug 14 19:52:40 2008 +0200
     2.3 @@ -87,15 +87,13 @@
     2.4  val output_known_symbols = implode oo (map o output_known_sym);
     2.5  val output_symbols = output_known_symbols (K true, K true);
     2.6  val output_syms = output_symbols o Symbol.explode;
     2.7 -val output_syms' = output_symbols o map #1 o SymbolPos.explode;
     2.8  
     2.9 -val output_syms_antiqs =
    2.10 -  Antiquote.read #> map
    2.11 +val output_syms_antiq =
    2.12    (fn Antiquote.Text s => output_syms s
    2.13 -    | Antiquote.Antiq x => enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_syms' x)
    2.14 +    | Antiquote.Antiq (ss, _) =>
    2.15 +        enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map SymbolPos.symbol ss))
    2.16      | Antiquote.Open _ => "{\\isaantiqopen}"
    2.17 -    | Antiquote.Close _ => "{\\isaantiqclose}") #>
    2.18 -  implode;
    2.19 +    | Antiquote.Close _ => "{\\isaantiqclose}");
    2.20  
    2.21  end;
    2.22  
    2.23 @@ -118,8 +116,11 @@
    2.24      else if T.is_kind T.AltString tok then
    2.25        enclose "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" (output_syms s)
    2.26      else if T.is_kind T.Verbatim tok then
    2.27 -      enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
    2.28 -        (output_syms_antiqs (s, T.position_of tok))
    2.29 +      let
    2.30 +        val (txt, pos) = T.source_of' tok;
    2.31 +        val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
    2.32 +        val out = implode (map output_syms_antiq ants);
    2.33 +      in enclose "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" out end
    2.34      else output_syms s
    2.35    end;
    2.36  
     3.1 --- a/src/Pure/Thy/thy_output.ML	Thu Aug 14 19:52:39 2008 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Aug 14 19:52:40 2008 +0200
     3.3 @@ -22,7 +22,7 @@
     3.4      (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.node option -> string
     3.5    datatype markup = Markup | MarkupEnv | Verbatim
     3.6    val modes: string list ref
     3.7 -  val eval_antiquote: Scan.lexicon -> Toplevel.node option -> string * Position.T -> string
     3.8 +  val eval_antiquote: Scan.lexicon -> Toplevel.node option -> SymbolPos.text * Position.T -> string
     3.9    val process_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    3.10      Toplevel.transition list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    3.11    val output_list: (Proof.context -> 'a -> Pretty.T) -> Args.src ->
    3.12 @@ -145,7 +145,7 @@
    3.13  
    3.14  val modes = ref ([]: string list);
    3.15  
    3.16 -fun eval_antiquote lex node (str, pos) =
    3.17 +fun eval_antiquote lex node (txt, pos) =
    3.18    let
    3.19      fun expand (Antiquote.Text s) = s
    3.20        | expand (Antiquote.Antiq x) =
    3.21 @@ -156,7 +156,7 @@
    3.22            end
    3.23        | expand (Antiquote.Open _) = ""
    3.24        | expand (Antiquote.Close _) = "";
    3.25 -    val ants = Antiquote.read (str, pos);
    3.26 +    val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
    3.27    in
    3.28      if is_none node andalso exists Antiquote.is_antiq ants then
    3.29        error ("Unknown context -- cannot expand text antiquotations" ^ Position.str_of pos)
    3.30 @@ -334,7 +334,7 @@
    3.31      fun markup mark mk flag = Scan.peek (fn d =>
    3.32        improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
    3.33        Scan.repeat tag --
    3.34 -      P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
    3.35 +      P.!!!! ((improper -- locale -- improper) |-- P.doc_source --| improper_end)
    3.36        >> (fn (((tok, pos), tags), txt) =>
    3.37          let val name = T.content_of tok
    3.38          in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
    3.39 @@ -347,7 +347,7 @@
    3.40          in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
    3.41  
    3.42      val cmt = Scan.peek (fn d =>
    3.43 -      P.$$$ "--" |-- P.!!!! (improper |-- P.position P.text)
    3.44 +      P.$$$ "--" |-- P.!!!! (improper |-- P.doc_source)
    3.45        >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
    3.46  
    3.47      val other = Scan.peek (fn d =>