more careful ML source positions, for improved PIDE markup;
authorwenzelm
Wed Nov 12 10:30:59 2014 +0100 (2014-11-12 ago)
changeset 5899192b6f4e68c5a
parent 58980 51890cb80b30
child 58992 584077922200
more careful ML source positions, for improved PIDE markup;
src/HOL/ex/Cartouche_Examples.thy
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ML/ml_context.ML
     1.1 --- a/src/HOL/ex/Cartouche_Examples.thy	Tue Nov 11 21:14:19 2014 +0100
     1.2 +++ b/src/HOL/ex/Cartouche_Examples.thy	Wed Nov 12 10:30:59 2014 +0100
     1.3 @@ -214,9 +214,10 @@
     1.4    fun ml_tactic source ctxt =
     1.5      let
     1.6        val ctxt' = ctxt |> Context.proof_map
     1.7 -        (ML_Context.expression (#range source)
     1.8 -          "fun tactic (ctxt : Proof.context) : tactic"
     1.9 -          "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source false source));
    1.10 +        (ML_Context.expression (#range source) "tactic" "Proof.context -> tactic"
    1.11 +          "Context.map_proof (ML_Tactic.set tactic)"
    1.12 +          (ML_Lex.read Position.none "fn ctxt: Proof.context =>" @
    1.13 +           ML_Lex.read_source false source));
    1.14      in Data.get ctxt' ctxt end;
    1.15  end;
    1.16  *}
     2.1 --- a/src/Pure/Isar/attrib.ML	Tue Nov 11 21:14:19 2014 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Wed Nov 12 10:30:59 2014 +0100
     2.3 @@ -208,8 +208,7 @@
     2.4  
     2.5  fun attribute_setup name source comment =
     2.6    ML_Lex.read_source false source
     2.7 -  |> ML_Context.expression (#range source)
     2.8 -    "val parser: Thm.attribute context_parser"
     2.9 +  |> ML_Context.expression (#range source) "parser" "Thm.attribute context_parser"
    2.10      ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    2.11        " parser " ^ ML_Syntax.print_string comment ^ ")")
    2.12    |> Context.proof_map;
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 21:14:19 2014 +0100
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Nov 12 10:30:59 2014 +0100
     3.3 @@ -60,14 +60,14 @@
     3.4  
     3.5  fun global_setup source =
     3.6    ML_Lex.read_source false source
     3.7 -  |> ML_Context.expression (#range source)
     3.8 -    "val setup: theory -> theory" "Context.map_theory setup"
     3.9 +  |> ML_Context.expression (#range source) "setup" "theory -> theory"
    3.10 +    "Context.map_theory setup"
    3.11    |> Context.theory_map;
    3.12  
    3.13  fun local_setup source =
    3.14    ML_Lex.read_source false source
    3.15 -  |> ML_Context.expression (#range source)
    3.16 -    "val local_setup: local_theory -> local_theory" "Context.map_proof local_setup"
    3.17 +  |> ML_Context.expression (#range source) "local_setup" "local_theory -> local_theory"
    3.18 +    "Context.map_proof local_setup"
    3.19    |> Context.proof_map;
    3.20  
    3.21  
    3.22 @@ -75,36 +75,36 @@
    3.23  
    3.24  fun parse_ast_translation source =
    3.25    ML_Lex.read_source false source
    3.26 -  |> ML_Context.expression (#range source)
    3.27 -    "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    3.28 +  |> ML_Context.expression (#range source) "parse_ast_translation"
    3.29 +    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    3.30      "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
    3.31    |> Context.theory_map;
    3.32  
    3.33  fun parse_translation source =
    3.34    ML_Lex.read_source false source
    3.35 -  |> ML_Context.expression (#range source)
    3.36 -    "val parse_translation: (string * (Proof.context -> term list -> term)) list"
    3.37 +  |> ML_Context.expression (#range source) "parse_translation"
    3.38 +    "(string * (Proof.context -> term list -> term)) list"
    3.39      "Context.map_theory (Sign.parse_translation parse_translation)"
    3.40    |> Context.theory_map;
    3.41  
    3.42  fun print_translation source =
    3.43    ML_Lex.read_source false source
    3.44 -  |> ML_Context.expression (#range source)
    3.45 -    "val print_translation: (string * (Proof.context -> term list -> term)) list"
    3.46 +  |> ML_Context.expression (#range source) "print_translation"
    3.47 +    "(string * (Proof.context -> term list -> term)) list"
    3.48      "Context.map_theory (Sign.print_translation print_translation)"
    3.49    |> Context.theory_map;
    3.50  
    3.51  fun typed_print_translation source =
    3.52    ML_Lex.read_source false source
    3.53 -  |> ML_Context.expression (#range source)
    3.54 -    "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
    3.55 +  |> ML_Context.expression (#range source) "typed_print_translation"
    3.56 +    "(string * (Proof.context -> typ -> term list -> term)) list"
    3.57      "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
    3.58    |> Context.theory_map;
    3.59  
    3.60  fun print_ast_translation source =
    3.61    ML_Lex.read_source false source
    3.62 -  |> ML_Context.expression (#range source)
    3.63 -    "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    3.64 +  |> ML_Context.expression (#range source) "print_ast_translation"
    3.65 +    "(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
    3.66      "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
    3.67    |> Context.theory_map;
    3.68  
    3.69 @@ -160,8 +160,7 @@
    3.70  
    3.71  fun declaration {syntax, pervasive} source =
    3.72    ML_Lex.read_source false source
    3.73 -  |> ML_Context.expression (#range source)
    3.74 -    "val declaration: Morphism.declaration"
    3.75 +  |> ML_Context.expression (#range source) "declaration" "Morphism.declaration"
    3.76      ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    3.77        \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
    3.78    |> Context.proof_map;
    3.79 @@ -171,8 +170,8 @@
    3.80  
    3.81  fun simproc_setup name lhss source identifier =
    3.82    ML_Lex.read_source false source
    3.83 -  |> ML_Context.expression (#range source)
    3.84 -    "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
    3.85 +  |> ML_Context.expression (#range source) "proc"
    3.86 +    "Morphism.morphism -> Proof.context -> cterm -> thm option"
    3.87      ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
    3.88        \lhss = " ^ ML_Syntax.print_strings lhss ^ ", proc = proc, \
    3.89        \identifier = Library.maps ML_Context.thms " ^ ML_Syntax.print_strings identifier ^ "})")
     4.1 --- a/src/Pure/Isar/method.ML	Tue Nov 11 21:14:19 2014 +0100
     4.2 +++ b/src/Pure/Isar/method.ML	Wed Nov 12 10:30:59 2014 +0100
     4.3 @@ -283,8 +283,10 @@
     4.4        let
     4.5          val context' = context |>
     4.6            ML_Context.expression (#range source)
     4.7 -            "fun tactic (morphism: Morphism.morphism) (facts: thm list) : tactic"
     4.8 -            "Method.set_tactic tactic" (ML_Lex.read_source false source);
     4.9 +            "tactic" "Morphism.morphism -> thm list -> tactic"
    4.10 +            "Method.set_tactic tactic"
    4.11 +            (ML_Lex.read Position.none "fn morphism: Morphism.morphism => fn facts: thm list =>" @
    4.12 +             ML_Lex.read_source false source);
    4.13          val tac = the_tactic context';
    4.14        in
    4.15          fn phi =>
    4.16 @@ -379,8 +381,8 @@
    4.17  
    4.18  fun method_setup name source comment =
    4.19    ML_Lex.read_source false source
    4.20 -  |> ML_Context.expression (#range source)
    4.21 -    "val parser: (Proof.context -> Proof.method) context_parser"
    4.22 +  |> ML_Context.expression (#range source) "parser"
    4.23 +    "(Proof.context -> Proof.method) context_parser"
    4.24      ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    4.25        " parser " ^ ML_Syntax.print_string comment ^ ")")
    4.26    |> Context.proof_map;
     5.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Tue Nov 11 21:14:19 2014 +0100
     5.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Nov 12 10:30:59 2014 +0100
     5.3 @@ -32,10 +32,12 @@
     5.4        end;
     5.5  
     5.6      fun reported_entity kind loc decl =
     5.7 -      let val pos = Exn_Properties.position_of loc in
     5.8 -        is_reported pos ?
     5.9 +      let
    5.10 +        val pos = Exn_Properties.position_of loc;
    5.11 +        val def_pos = Exn_Properties.position_of decl;
    5.12 +      in
    5.13 +        (is_reported pos andalso pos <> def_pos) ?
    5.14            let
    5.15 -            val def_pos = Exn_Properties.position_of decl;
    5.16              fun markup () =
    5.17                (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of def_pos);
    5.18            in cons (pos, markup, fn () => "") end
     6.1 --- a/src/Pure/ML/ml_context.ML	Tue Nov 11 21:14:19 2014 +0100
     6.2 +++ b/src/Pure/ML/ml_context.ML	Wed Nov 12 10:30:59 2014 +0100
     6.3 @@ -25,7 +25,7 @@
     6.4    val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
     6.5      ML_Lex.token Antiquote.antiquote list -> unit
     6.6    val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
     6.7 -  val expression: Position.range -> string -> string ->
     6.8 +  val expression: Position.range -> string -> string -> string ->
     6.9      ML_Lex.token Antiquote.antiquote list -> Context.generic -> Context.generic
    6.10  end
    6.11  
    6.12 @@ -183,14 +183,15 @@
    6.13    Context.setmp_thread_data (Option.map Context.Proof ctxt)
    6.14      (fn () => eval_source flags source) ();
    6.15  
    6.16 -fun expression range bind body ants =
    6.17 +fun expression range name constraint body ants =
    6.18    let
    6.19      val hidden = ML_Lex.read Position.none;
    6.20      val visible = ML_Lex.read_set_range range;
    6.21    in
    6.22      exec (fn () =>
    6.23        eval ML_Compiler.flags (#1 range)
    6.24 -       (hidden "Context.set_thread_data (SOME (let" @ visible bind @ hidden "=" @ ants @
    6.25 +       (hidden "Context.set_thread_data (SOME (let val " @ visible name @
    6.26 +        hidden (": " ^ constraint ^ " =") @ ants @
    6.27          hidden ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")))
    6.28    end;
    6.29