more careful ML source positions, for improved PIDE markup;
authorwenzelm
Tue Nov 11 20:11:38 2014 +0100 (2014-11-11 ago)
changeset 58979162a4c2e97bc
parent 58978 e42da880c61e
child 58980 51890cb80b30
more careful ML source positions, for improved PIDE markup;
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/method.ML
src/Pure/ML/ml_context.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Nov 11 18:16:25 2014 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Nov 11 20:11:38 2014 +0100
     1.3 @@ -206,13 +206,12 @@
     1.4  fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
     1.5  fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
     1.6  
     1.7 -fun attribute_setup name source cmt =
     1.8 -  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
     1.9 -    ML_Lex.read_source false source @
    1.10 -    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
    1.11 +fun attribute_setup name source comment =
    1.12 +  ML_Lex.read_source false source
    1.13    |> ML_Context.expression (#range source)
    1.14 -    "val (name, scan, comment): binding * attribute context_parser * string"
    1.15 -    "Context.map_proof (Attrib.local_setup name scan comment)"
    1.16 +    "val parser: Thm.attribute context_parser"
    1.17 +    ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    1.18 +      " parser " ^ ML_Syntax.print_string comment ^ ")")
    1.19    |> Context.proof_map;
    1.20  
    1.21  
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 18:16:25 2014 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 11 20:11:38 2014 +0100
     2.3 @@ -67,7 +67,7 @@
     2.4  fun local_setup source =
     2.5    ML_Lex.read_source false source
     2.6    |> ML_Context.expression (#range source)
     2.7 -    "val setup: local_theory -> local_theory" "Context.map_proof setup"
     2.8 +    "val local_setup: local_theory -> local_theory" "Context.map_proof local_setup"
     2.9    |> Context.proof_map;
    2.10  
    2.11  
     3.1 --- a/src/Pure/Isar/method.ML	Tue Nov 11 18:16:25 2014 +0100
     3.2 +++ b/src/Pure/Isar/method.ML	Tue Nov 11 20:11:38 2014 +0100
     3.3 @@ -377,13 +377,12 @@
     3.4  fun setup binding scan comment = define_global binding (method_syntax scan) comment #> snd;
     3.5  fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
     3.6  
     3.7 -fun method_setup name source cmt =
     3.8 -  (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
     3.9 -    ML_Lex.read_source false source @
    3.10 -    ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")"))
    3.11 +fun method_setup name source comment =
    3.12 +  ML_Lex.read_source false source
    3.13    |> ML_Context.expression (#range source)
    3.14 -    "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
    3.15 -    "Context.map_proof (Method.local_setup name scan comment)"
    3.16 +    "val parser: (Proof.context -> Proof.method) context_parser"
    3.17 +    ("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
    3.18 +      " parser " ^ ML_Syntax.print_string comment ^ ")")
    3.19    |> Context.proof_map;
    3.20  
    3.21  
     4.1 --- a/src/Pure/ML/ml_context.ML	Tue Nov 11 18:16:25 2014 +0100
     4.2 +++ b/src/Pure/ML/ml_context.ML	Tue Nov 11 20:11:38 2014 +0100
     4.3 @@ -184,11 +184,15 @@
     4.4      (fn () => eval_source flags source) ();
     4.5  
     4.6  fun expression range bind body ants =
     4.7 -  exec (fn () =>
     4.8 -    eval ML_Compiler.flags (#1 range)
     4.9 -     (ML_Lex.read_set_range range ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @
    4.10 -      ants @
    4.11 -      ML_Lex.read_set_range range (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
    4.12 +  let
    4.13 +    val hidden = ML_Lex.read Position.none;
    4.14 +    val visible = ML_Lex.read_set_range range;
    4.15 +  in
    4.16 +    exec (fn () =>
    4.17 +      eval ML_Compiler.flags (#1 range)
    4.18 +       (hidden "Context.set_thread_data (SOME (let" @ visible bind @ hidden "=" @ ants @
    4.19 +        hidden ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")))
    4.20 +  end;
    4.21  
    4.22  end;
    4.23