more careful ML source positions, for improved PIDE markup;
authorwenzelm
Sat Nov 22 13:38:15 2014 +0100 (2014-11-22 ago)
changeset 59029c907cbe36713
parent 59028 df7476e79558
child 59030 67baff6f697c
more careful ML source positions, for improved PIDE markup;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/parse.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Nov 22 11:36:00 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Nov 22 13:38:15 2014 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    val print_ast_translation: Symbol_Pos.source -> theory -> theory
     1.5    val translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.6    val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory
     1.7 -  val oracle: bstring * Position.T -> Symbol_Pos.source -> theory -> theory
     1.8 +  val oracle: bstring * Position.range -> Symbol_Pos.source -> theory -> theory
     1.9    val add_defs: (bool * bool) * ((binding * string) * Token.src list) list -> theory -> theory
    1.10    val declaration: {syntax: bool, pervasive: bool} ->
    1.11      Symbol_Pos.source -> local_theory -> local_theory
    1.12 @@ -127,21 +127,25 @@
    1.13  
    1.14  (* oracles *)
    1.15  
    1.16 -fun oracle (name, pos) source =
    1.17 +fun oracle (name, range) source =
    1.18    let
    1.19 +    val body_range = #range source;
    1.20      val body = ML_Lex.read_source false source;
    1.21 +
    1.22 +    val hidden = ML_Lex.read Position.none;
    1.23 +    val visible = ML_Lex.read_set_range;
    1.24      val ants =
    1.25 -      ML_Lex.read Position.none
    1.26 +      hidden
    1.27         ("local\n\
    1.28 -        \  val binding = " ^ ML_Syntax.make_binding (name, pos) ^ ";\n\
    1.29 -        \  val body = ") @ body @ ML_Lex.read Position.none (";\n\
    1.30 +        \  val binding = " ^ ML_Syntax.make_binding (name, #1 range) ^ ";\n\
    1.31 +        \  val") @ visible body_range "oracle" @ hidden "=" @ body @ hidden (";\n\
    1.32          \in\n\
    1.33 -        \  val " ^ name ^
    1.34 -        " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
    1.35 -        \end;\n");
    1.36 +        \  val") @ visible range name @ hidden "=\
    1.37 +        \ snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
    1.38 +        \end;\n";
    1.39    in
    1.40      Context.theory_map
    1.41 -      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 (#range source)) ants))
    1.42 +      (ML_Context.exec (fn () => ML_Context.eval ML_Compiler.flags (#1 body_range) ants))
    1.43    end;
    1.44  
    1.45  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Nov 22 11:36:00 2014 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Nov 22 13:38:15 2014 +0100
     2.3 @@ -326,7 +326,7 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.command @{command_spec "oracle"} "declare oracle"
     2.7 -    (Parse.position Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
     2.8 +    (Parse.range Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
     2.9        (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
    2.10  
    2.11  
     3.1 --- a/src/Pure/Isar/parse.ML	Sat Nov 22 11:36:00 2014 +0100
     3.2 +++ b/src/Pure/Isar/parse.ML	Sat Nov 22 13:38:15 2014 +0100
     3.3 @@ -14,6 +14,7 @@
     3.4    val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
     3.5    val not_eof: Token.T parser
     3.6    val token: 'a parser -> Token.T parser
     3.7 +  val range: 'a parser -> ('a * Position.range) parser
     3.8    val position: 'a parser -> ('a * Position.T) parser
     3.9    val source_position: 'a parser -> Symbol_Pos.source parser
    3.10    val inner_syntax: 'a parser -> string parser
    3.11 @@ -172,6 +173,7 @@
    3.12  
    3.13  fun token atom = Scan.ahead not_eof --| atom;
    3.14  
    3.15 +fun range scan = (Scan.ahead not_eof >> (Token.range_of o single)) -- scan >> Library.swap;
    3.16  fun position scan = (Scan.ahead not_eof >> Token.pos_of) -- scan >> Library.swap;
    3.17  fun source_position atom = Scan.ahead atom |-- not_eof >> Token.source_position_of;
    3.18  fun inner_syntax atom = Scan.ahead atom |-- not_eof >> Token.inner_syntax_of;