datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
authorwenzelm
Tue Mar 24 11:57:41 2009 +0100 (2009-03-24)
changeset 30683e8ac1f9d9469
parent 30682 dcb233670c98
child 30696 5f0919630aaa
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
src/Pure/General/antiquote.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_lex.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Tue Mar 24 11:39:25 2009 +0100
     1.2 +++ b/src/Pure/General/antiquote.ML	Tue Mar 24 11:57:41 2009 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  sig
     1.5    datatype 'a antiquote =
     1.6      Text of 'a |
     1.7 -    Antiq of Symbol_Pos.T list * Position.T |
     1.8 +    Antiq of Symbol_Pos.T list * Position.range |
     1.9      Open of Position.T |
    1.10      Close of Position.T
    1.11    val is_text: 'a antiquote -> bool
    1.12 @@ -26,7 +26,7 @@
    1.13  
    1.14  datatype 'a antiquote =
    1.15    Text of 'a |
    1.16 -  Antiq of Symbol_Pos.T list * Position.T |
    1.17 +  Antiq of Symbol_Pos.T list * Position.range |
    1.18    Open of Position.T |
    1.19    Close of Position.T;
    1.20  
    1.21 @@ -39,7 +39,7 @@
    1.22  val report_antiq = Position.report Markup.antiq;
    1.23  
    1.24  fun report report_text (Text x) = report_text x
    1.25 -  | report _ (Antiq (_, pos)) = report_antiq pos
    1.26 +  | report _ (Antiq (_, (pos, _))) = report_antiq pos
    1.27    | report _ (Open pos) = report_antiq pos
    1.28    | report _ (Close pos) = report_antiq pos;
    1.29  
    1.30 @@ -79,7 +79,7 @@
    1.31    Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
    1.32      Symbol_Pos.!!! "missing closing brace of antiquotation"
    1.33        (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
    1.34 -  >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
    1.35 +  >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
    1.36  
    1.37  val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
    1.38  val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
     2.1 --- a/src/Pure/ML/ml_context.ML	Tue Mar 24 11:39:25 2009 +0100
     2.2 +++ b/src/Pure/ML/ml_context.ML	Tue Mar 24 11:57:41 2009 +0100
     2.3 @@ -219,12 +219,12 @@
     2.4            fun no_decl _ = ([], []);
     2.5  
     2.6            fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
     2.7 -            | expand (Antiquote.Antiq x) (scope, background) =
     2.8 +            | expand (Antiquote.Antiq (ss, range)) (scope, background) =
     2.9                  let
    2.10                    val context = Stack.top scope;
    2.11 -                  val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
    2.12 +                  val (f, context') = antiquotation (T.read_antiq lex antiq (ss, #1 range)) context;
    2.13                    val (decl, background') = f {background = background, struct_name = struct_name};
    2.14 -                  val decl' = pairself ML_Lex.tokenize o decl;
    2.15 +                  val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
    2.16                  in (decl', (Stack.map_top (K context') scope, background')) end
    2.17              | expand (Antiquote.Open _) (scope, background) =
    2.18                  (no_decl, (Stack.push scope, background))
     3.1 --- a/src/Pure/ML/ml_lex.ML	Tue Mar 24 11:39:25 2009 +0100
     3.2 +++ b/src/Pure/ML/ml_lex.ML	Tue Mar 24 11:57:41 2009 +0100
     3.3 @@ -13,6 +13,7 @@
     3.4    val stopper: token Scan.stopper
     3.5    val is_regular: token -> bool
     3.6    val is_improper: token -> bool
     3.7 +  val set_range: Position.range -> token -> token
     3.8    val pos_of: token -> Position.T
     3.9    val kind_of: token -> token_kind
    3.10    val content_of: token -> string
    3.11 @@ -42,6 +43,8 @@
    3.12  
    3.13  (* position *)
    3.14  
    3.15 +fun set_range range (Token (_, x)) = Token (range, x);
    3.16 +
    3.17  fun pos_of (Token ((pos, _), _)) = pos;
    3.18  fun end_pos_of (Token ((_, pos), _)) = pos;
    3.19  
     4.1 --- a/src/Pure/Thy/thy_output.ML	Tue Mar 24 11:39:25 2009 +0100
     4.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Mar 24 11:57:41 2009 +0100
     4.3 @@ -148,8 +148,8 @@
     4.4  fun eval_antiquote lex state (txt, pos) =
     4.5    let
     4.6      fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
     4.7 -      | expand (Antiquote.Antiq x) =
     4.8 -          let val (opts, src) = T.read_antiq lex antiq x in
     4.9 +      | expand (Antiquote.Antiq (ss, (pos, _))) =
    4.10 +          let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
    4.11              options opts (fn () => command src state) ();  (*preview errors!*)
    4.12              PrintMode.with_modes (! modes @ Latex.modes)
    4.13                (Output.no_warnings (options opts (fn () => command src state))) ()