Antiquote.Text: keep full position information;
authorwenzelm
Thu Mar 19 15:44:14 2009 +0100 (2009-03-19)
changeset 30589cbe27c4ef417
parent 30588 05f81bbb2614
child 30590 1d9c9fcf8513
Antiquote.Text: keep full position information;
src/Pure/General/antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Thu Mar 19 15:22:53 2009 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Thu Mar 19 15:44:14 2009 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature ANTIQUOTE =
     1.5  sig
     1.6    datatype antiquote =
     1.7 -    Text of string | Antiq of Symbol_Pos.T list * Position.T |
     1.8 +    Text of Symbol_Pos.T list | Antiq of Symbol_Pos.T list * Position.T |
     1.9      Open of Position.T | Close of Position.T
    1.10    val is_antiq: antiquote -> bool
    1.11    val read: Symbol_Pos.T list * Position.T -> antiquote list
    1.12 @@ -19,7 +19,7 @@
    1.13  (* datatype antiquote *)
    1.14  
    1.15  datatype antiquote =
    1.16 -  Text of string |
    1.17 +  Text of Symbol_Pos.T list |
    1.18    Antiq of Symbol_Pos.T list * Position.T |
    1.19    Open of Position.T |
    1.20    Close of Position.T;
    1.21 @@ -68,7 +68,7 @@
    1.22  in
    1.23  
    1.24  val scan_antiquote =
    1.25 - (Scan.repeat1 scan_txt >> (Text o Symbol_Pos.content o flat) ||
    1.26 + (Scan.repeat1 scan_txt >> (Text o flat) ||
    1.27    scan_antiq ||
    1.28    Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open ||
    1.29    Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close);
     2.1 --- a/src/Pure/ML/ml_context.ML	Thu Mar 19 15:22:53 2009 +0100
     2.2 +++ b/src/Pure/ML/ml_context.ML	Thu Mar 19 15:44:14 2009 +0100
     2.3 @@ -210,7 +210,8 @@
     2.4            val lex = #1 (OuterKeyword.get_lexicons ());
     2.5            fun no_decl _ = ("", "");
     2.6  
     2.7 -          fun expand (Antiquote.Text s) state = (K ("", Symbol.escape s), state)
     2.8 +          fun expand (Antiquote.Text ss) state =
     2.9 +                (K ("", Symbol.escape (Symbol_Pos.content ss)), state)
    2.10              | expand (Antiquote.Antiq x) (scope, background) =
    2.11                  let
    2.12                    val context = Stack.top scope;
     3.1 --- a/src/Pure/Thy/latex.ML	Thu Mar 19 15:22:53 2009 +0100
     3.2 +++ b/src/Pure/Thy/latex.ML	Thu Mar 19 15:44:14 2009 +0100
     3.3 @@ -88,7 +88,7 @@
     3.4  val output_syms = output_symbols o Symbol.explode;
     3.5  
     3.6  val output_syms_antiq =
     3.7 -  (fn Antiquote.Text s => output_syms s
     3.8 +  (fn Antiquote.Text ss => output_symbols (map Symbol_Pos.symbol ss)
     3.9      | Antiquote.Antiq (ss, _) =>
    3.10          enclose "%\n\\isaantiq\n" "%\n\\endisaantiq\n" (output_symbols (map Symbol_Pos.symbol ss))
    3.11      | Antiquote.Open _ => "{\\isaantiqopen}"
     4.1 --- a/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:22:53 2009 +0100
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Mar 19 15:44:14 2009 +0100
     4.3 @@ -147,7 +147,7 @@
     4.4  
     4.5  fun eval_antiquote lex state (txt, pos) =
     4.6    let
     4.7 -    fun expand (Antiquote.Text s) = s
     4.8 +    fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
     4.9        | expand (Antiquote.Antiq x) =
    4.10            let val (opts, src) = T.read_antiq lex antiq x in
    4.11              options opts (fn () => command src state) ();  (*preview errors!*)