--- 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);
--- 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;
*}
--- 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
--- 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
--- 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;
--- 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
--- 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 []));