more robust ML antiquotations -- allow original tokens without adjacent whitespace;
authorwenzelm
Tue Dec 21 21:05:50 2010 +0100 (2010-12-21)
changeset 4137608240feb69c7
parent 41375 7a89b4b94817
child 41377 390c53904220
more robust ML antiquotations -- allow original tokens without adjacent whitespace;
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_thms.ML
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Pure/ML/ml_antiquote.ML	Tue Dec 21 19:35:36 2010 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquote.ML	Tue Dec 21 21:05:50 2010 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4      let
     1.5        val (a, background') = variant (translate_string (fn "." => "_" | c => c) name) background;
     1.6        val env = kind ^ " " ^ a ^ " = " ^ s ^ ";\n";
     1.7 -      val body = "Isabelle." ^ a;
     1.8 +      val body = " Isabelle." ^ a ^ " ";
     1.9      in (K (env, body), background') end));
    1.10  
    1.11  val value = declaration "val";
     2.1 --- a/src/Pure/ML/ml_thms.ML	Tue Dec 21 19:35:36 2010 +0100
     2.2 +++ b/src/Pure/ML/ml_thms.ML	Tue Dec 21 21:05:50 2010 +0100
     2.3 @@ -39,7 +39,7 @@
     2.4        val i = serial ();
     2.5        val (a, background') = background
     2.6          |> ML_Antiquote.variant kind ||> put_thms (i, ths);
     2.7 -      val ml = (thm_bind kind a i, "Isabelle." ^ a);
     2.8 +      val ml = (thm_bind kind a i, " Isabelle." ^ a ^ " ");
     2.9      in (K ml, background') end));
    2.10  
    2.11  val _ = thm_antiq "thm" (Attrib.thm >> single);
    2.12 @@ -69,7 +69,8 @@
    2.13          val (a, background') = background
    2.14            |> ML_Antiquote.variant "lemma" ||> put_thms (i, the_thms ctxt' i);
    2.15          val ml =
    2.16 -          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i, "Isabelle." ^ a);
    2.17 +          (thm_bind (if length (flat propss) = 1 then "thm" else "thms") a i,
    2.18 +            " Isabelle." ^ a ^ " ");
    2.19        in (K ml, background') end));
    2.20  
    2.21  end;
     3.1 --- a/src/Tools/Code/code_runtime.ML	Tue Dec 21 19:35:36 2010 +0100
     3.2 +++ b/src/Tools/Code/code_runtime.ML	Tue Dec 21 21:05:50 2010 +0100
     3.3 @@ -228,16 +228,13 @@
     3.4  
     3.5  fun register_const const = register_code [] [const];
     3.6  
     3.7 -fun print_const const all_struct_name consts_map =
     3.8 -  (Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const;
     3.9 -
    3.10  fun print_code is_first const ctxt =
    3.11    let
    3.12      val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt;
    3.13      val (ml_code, consts_map) = Lazy.force acc_code;
    3.14      val ml_code = if is_first then ml_code else "";
    3.15 -    val all_struct_name = "Isabelle";
    3.16 -  in (ml_code, print_const const all_struct_name consts_map) end;
    3.17 +    val body = " Isabelle." ^ the (AList.lookup (op =) consts_map const) ^ " ";
    3.18 +  in (ml_code, body) end;
    3.19  
    3.20  in
    3.21