# HG changeset patch
# User wenzelm
# Date 1417352568 -3600
# Node ID dd8ec9138112535691a5204c3185feae77e22ae4
# Parent  45ab32a542fe39356457bf83e98fe404c50fc4d0
tuned signature;

diff -r 45ab32a542fe -r dd8ec9138112 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 14:02:48 2014 +0100
@@ -37,28 +37,29 @@
 
 local
 
-val ml_toks = ML_Lex.read Position.none;
+fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");"
+  | ml_val (toks1, toks2) =
+      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
 
-fun ml_val (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks ");"
-  | ml_val (toks1, toks2) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
-
-fun ml_op (toks1, []) = ml_toks "fn _ => (op " @ toks1 @ ml_toks ");"
-  | ml_op (toks1, toks2) = ml_toks "fn _ => (op " @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
+fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");"
+  | ml_op (toks1, toks2) =
+      ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
 
-fun ml_type (toks1, []) = ml_toks "val _ = NONE : (" @ toks1 @ ml_toks ") option;"
+fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;"
   | ml_type (toks1, toks2) =
-      ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
-        toks2 @ ml_toks ") option];";
+      ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @
+        toks2 @ ML_Lex.read ") option];";
 
-fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
+fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);"
   | ml_exception (toks1, toks2) =
-      ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
+      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);";
 
 fun ml_structure (toks, _) =
-  ml_toks "functor XXX() = struct structure XX = " @ toks @ ml_toks " end;";
+  ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;";
 
 fun ml_functor (Antiquote.Text tok :: _, _) =
-      ml_toks "ML_Env.check_functor " @ ml_toks (ML_Syntax.print_string (ML_Lex.content_of tok))
+      ML_Lex.read "ML_Env.check_functor " @
+      ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
   | ml_functor _ = raise Fail "Bad ML functor specification";
 
 val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent);
diff -r 45ab32a542fe -r dd8ec9138112 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Sun Nov 30 14:02:48 2014 +0100
@@ -142,10 +142,7 @@
   Thy_Output.antiquotation @{binding ML_cartouche}
     (Scan.lift Args.cartouche_source_position) (fn {context, ...} => fn source =>
       let
-        val toks =
-          ML_Lex.read Position.none "fn _ => (" @
-          ML_Lex.read_source false source @
-          ML_Lex.read Position.none ");";
+        val toks = ML_Lex.read "fn _ => (" @ ML_Lex.read_source false source @ ML_Lex.read ");";
         val _ = ML_Context.eval_in (SOME context) ML_Compiler.flags (Input.pos_of source) toks;
       in "" end);
 *}
@@ -215,8 +212,7 @@
       val ctxt' = ctxt |> Context.proof_map
         (ML_Context.expression (Input.range_of source) "tactic" "Proof.context -> tactic"
           "Context.map_proof (ML_Tactic.set tactic)"
-          (ML_Lex.read Position.none "fn ctxt: Proof.context =>" @
-           ML_Lex.read_source false source));
+          (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source));
     in Data.get ctxt' ctxt end;
 end;
 *}
diff -r 45ab32a542fe -r dd8ec9138112 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 30 14:02:48 2014 +0100
@@ -131,15 +131,13 @@
     val body_range = Input.range_of source;
     val body = ML_Lex.read_source false source;
 
-    val hidden = ML_Lex.read Position.none;
-    val visible = ML_Lex.read_set_range;
     val ants =
-      hidden
+      ML_Lex.read
        ("local\n\
         \  val binding = " ^ ML_Syntax.make_binding (name, #1 range) ^ ";\n\
-        \  val") @ visible body_range "oracle" @ hidden "=" @ body @ hidden (";\n\
-        \in\n\
-        \  val") @ visible range name @ hidden "=\
+        \  val") @ ML_Lex.read_set_range body_range "oracle" @ ML_Lex.read "=" @ body @
+        ML_Lex.read (";\nin\n\
+        \  val") @ ML_Lex.read_set_range range name @ ML_Lex.read "=\
         \ snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, oracle))));\n\
         \end;\n";
   in
diff -r 45ab32a542fe -r dd8ec9138112 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/Pure/Isar/method.ML	Sun Nov 30 14:02:48 2014 +0100
@@ -284,7 +284,7 @@
           ML_Context.expression (Input.range_of source)
             "tactic" "Morphism.morphism -> thm list -> tactic"
             "Method.set_tactic tactic"
-            (ML_Lex.read Position.none "fn morphism: Morphism.morphism => fn facts: thm list =>" @
+            (ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
              ML_Lex.read_source false source);
         val tac = the_tactic context';
       in
diff -r 45ab32a542fe -r dd8ec9138112 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Sun Nov 30 14:02:48 2014 +0100
@@ -170,7 +170,7 @@
 
 fun eval_file flags path =
   let val pos = Path.position path
-  in eval flags pos (ML_Lex.read pos (File.read path)) end;
+  in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
 
 fun eval_source flags source =
   eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
@@ -184,16 +184,11 @@
     (fn () => eval_source flags source) ();
 
 fun expression range name constraint body ants =
-  let
-    val hidden = ML_Lex.read Position.none;
-    val visible = ML_Lex.read_set_range range;
-  in
-    exec (fn () =>
-      eval ML_Compiler.flags (#1 range)
-       (hidden "Context.set_thread_data (SOME (let val " @ visible name @
-        hidden (": " ^ constraint ^ " =") @ ants @
-        hidden ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")))
-  end;
+  exec (fn () =>
+    eval ML_Compiler.flags (#1 range)
+     (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
+      ML_Lex.read (": " ^ constraint ^ " =") @ ants @
+      ML_Lex.read ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
 
 end;
 
diff -r 45ab32a542fe -r dd8ec9138112 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Sun Nov 30 14:02:48 2014 +0100
@@ -25,7 +25,8 @@
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
       Source.source) Source.source
   val tokenize: string -> token list
-  val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
+  val read_pos: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
+  val read: Symbol_Pos.text -> token Antiquote.antiquote list
   val read_set_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
   val read_source: bool -> Input.source -> token Antiquote.antiquote list
 end;
@@ -324,11 +325,12 @@
 
 val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
 
-val read = gen_read false;
+val read_pos = gen_read false;
+
+val read = read_pos Position.none;
 
 fun read_set_range range =
-  read Position.none
-  #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
+  read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
 
 fun read_source SML source =
   let
diff -r 45ab32a542fe -r dd8ec9138112 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sun Nov 30 14:02:48 2014 +0100
@@ -671,9 +671,7 @@
     verbatim_text ctxt (Input.source_content source)));
 
 fun ml_enclose bg en source =
-  ML_Lex.read Position.none bg @
-  ML_Lex.read_source false source @
-  ML_Lex.read Position.none en;
+  ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
 
 in
 
@@ -686,7 +684,7 @@
 
   ml_text @{binding ML_functor}   (* FIXME formal treatment of functor name (!?) *)
     (fn source =>
-      ML_Lex.read Position.none ("ML_Env.check_functor " ^
+      ML_Lex.read ("ML_Env.check_functor " ^
         ML_Syntax.print_string (Input.source_content source))) #>
 
   ml_text @{binding ML_text} (K []));