--- a/src/Doc/antiquote_setup.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Doc/antiquote_setup.ML Mon Aug 27 20:43:01 2018 +0200
@@ -71,7 +71,7 @@
| _ => error ("Single ML name expected in input: " ^ quote txt));
fun prep_ml source =
- (Input.source_content source, ML_Lex.read_source false source);
+ (Input.source_content source, ML_Lex.read_source source);
fun index_ml name kind ml = Thy_Output.antiquotation_raw name
(Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
--- a/src/HOL/ex/Cartouche_Examples.thy Mon Aug 27 19:29:07 2018 +0200
+++ b/src/HOL/ex/Cartouche_Examples.thy Mon Aug 27 20:43:01 2018 +0200
@@ -178,7 +178,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 "fn ctxt: Proof.context =>" @ ML_Lex.read_source false source));
+ (ML_Lex.read "fn ctxt: Proof.context =>" @ ML_Lex.read_source source));
in Data.get ctxt' ctxt end;
end;
\<close>
--- a/src/Pure/Isar/attrib.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/Isar/attrib.ML Mon Aug 27 20:43:01 2018 +0200
@@ -215,7 +215,7 @@
fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
fun attribute_setup name source comment =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser"
("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
" parser " ^ ML_Syntax.print_string comment ^ ")")
--- a/src/Pure/Isar/isar_cmd.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Mon Aug 27 20:43:01 2018 +0200
@@ -51,13 +51,13 @@
(* generic setup *)
fun setup source =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "setup" "theory -> theory"
"Context.map_theory setup"
|> Context.theory_map;
fun local_setup source =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "local_setup" "local_theory -> local_theory"
"Context.map_proof local_setup"
|> Context.proof_map;
@@ -66,35 +66,35 @@
(* translation functions *)
fun parse_ast_translation source =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "parse_ast_translation"
"(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
|> Context.theory_map;
fun parse_translation source =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "parse_translation"
"(string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.parse_translation parse_translation)"
|> Context.theory_map;
fun print_translation source =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "print_translation"
"(string * (Proof.context -> term list -> term)) list"
"Context.map_theory (Sign.print_translation print_translation)"
|> Context.theory_map;
fun typed_print_translation source =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "typed_print_translation"
"(string * (Proof.context -> typ -> term list -> term)) list"
"Context.map_theory (Sign.typed_print_translation typed_print_translation)"
|> Context.theory_map;
fun print_ast_translation source =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "print_ast_translation"
"(string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
"Context.map_theory (Sign.print_ast_translation print_ast_translation)"
@@ -122,7 +122,7 @@
fun oracle (name, range) source =
let
val body_range = Input.range_of source;
- val body = ML_Lex.read_source false source;
+ val body = ML_Lex.read_source source;
val ants =
ML_Lex.read
@@ -142,7 +142,7 @@
(* declarations *)
fun declaration {syntax, pervasive} source =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "declaration" "Morphism.declaration"
("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
\pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
@@ -152,7 +152,7 @@
(* simprocs *)
fun simproc_setup name lhss source =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "proc"
"Morphism.morphism -> Proof.context -> cterm -> thm option"
("Context.map_proof (Simplifier.define_simproc_cmd " ^
--- a/src/Pure/Isar/method.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/Isar/method.ML Mon Aug 27 20:43:01 2018 +0200
@@ -373,7 +373,7 @@
"tactic" "Morphism.morphism -> thm list -> tactic"
"Method.set_tactic tactic"
(ML_Lex.read "fn morphism: Morphism.morphism => fn facts: thm list =>" @
- ML_Lex.read_source false source);
+ ML_Lex.read_source source);
val tac = the_tactic context';
in
fn phi => set_tactic (fn _ => Context.setmp_generic_context (SOME context) (tac phi))
@@ -476,7 +476,7 @@
fun local_setup binding scan comment = define binding (method_syntax scan) comment #> snd;
fun method_setup name source comment =
- ML_Lex.read_source false source
+ ML_Lex.read_source source
|> ML_Context.expression (Input.range_of source) "parser"
"(Proof.context -> Proof.method) context_parser"
("Context.map_proof (Method.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
--- a/src/Pure/ML/ml_context.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/ML/ml_context.ML Mon Aug 27 20:43:01 2018 +0200
@@ -192,7 +192,7 @@
fun eval_file flags path =
let val pos = Path.position path
- in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
+ in eval flags pos (ML_Lex.read_text (File.read path, pos)) end;
fun eval_source flags source =
let
--- a/src/Pure/ML/ml_env.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/ML/ml_env.ML Mon Aug 27 20:43:01 2018 +0200
@@ -174,12 +174,13 @@
Name_Space.define (Context.Theory thy') true (Binding.name env_name, (tables, ops)) envs;
in envs' end);
-fun make_operations SML: operations =
- {read_source = ML_Lex.read_source SML,
- explode_token = ML_Lex.explode_content_of SML};
+val Isabelle_operations: operations =
+ {read_source = ML_Lex.read_source,
+ explode_token = ML_Lex.check_content_of #> Symbol.explode #> maps (Symbol.esc #> String.explode)};
-val Isabelle_operations = make_operations false;
-val SML_operations = make_operations true;
+val SML_operations: operations =
+ {read_source = ML_Lex.read_source_sml,
+ explode_token = ML_Lex.check_content_of #> String.explode};
val _ = Theory.setup (setup Isabelle Isabelle_operations #> setup SML SML_operations);
--- a/src/Pure/ML/ml_lex.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/ML/ml_lex.ML Mon Aug 27 20:43:01 2018 +0200
@@ -22,16 +22,18 @@
val kind_of: token -> token_kind
val content_of: token -> string
val check_content_of: token -> string
- val explode_content_of: bool -> token -> char list
val flatten: token list -> string
val source: (Symbol.symbol, 'a) Source.source ->
(token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
Source.source) Source.source
val tokenize: string -> token list
- val read_pos: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
+ val read_text: Symbol_Pos.text * Position.T -> 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
+ val read_source': {language: bool -> Markup.T, opaque_warning: bool, symbols: bool} ->
+ token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
+ val read_source: Input.source -> token Antiquote.antiquote list
+ val read_source_sml: Input.source -> token Antiquote.antiquote list
end;
structure ML_Lex: ML_LEX =
@@ -115,7 +117,7 @@
fun is_comment (Token (_, (Comment _, _))) = true
| is_comment _ = false;
-fun warn tok =
+fun warning_opaque tok =
(case tok of
Token (_, (Keyword, ":>")) =>
warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
@@ -128,10 +130,6 @@
Error msg => error msg
| _ => content_of tok);
-fun explode_content_of SML =
- check_content_of #>
- (if SML then String.explode else Symbol.explode #> maps (Symbol.esc #> String.explode));
-
(* flatten *)
@@ -310,12 +308,14 @@
scan_ident >> token Ident ||
scan_type_var >> token Type_Var);
+val scan_sml_antiq = scan_sml >> Antiquote.Text;
+
val scan_ml_antiq =
Comment.scan >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
Antiquote.scan_control >> Antiquote.Control ||
Antiquote.scan_antiq >> Antiquote.Antiq ||
scan_rat_antiq >> Antiquote.Antiq ||
- scan_sml >> Antiquote.Text;
+ scan_sml_antiq;
fun recover msg =
(recover_char ||
@@ -325,12 +325,8 @@
Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
>> (single o token (Error msg));
-fun gen_read SML pos text =
+fun reader {opaque_warning} scan syms =
let
- val syms =
- Symbol_Pos.explode (text, pos)
- |> SML ? maps (fn (s, p) => raw_explode s |> map (rpair p));
-
val termination =
if null syms then []
else
@@ -339,8 +335,8 @@
val pos2 = Position.advance Symbol.space pos1;
in [Antiquote.Text (Token (Position.range (pos1, pos2), (Space, Symbol.space)))] end;
- val scan = if SML then scan_sml >> Antiquote.Text else scan_ml_antiq;
- fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)
+ fun check (Antiquote.Text tok) =
+ (check_content_of tok; if opaque_warning then warning_opaque tok else ())
| check _ = ();
val input =
Source.of_list syms
@@ -361,22 +357,31 @@
val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust;
-val read_pos = gen_read false;
-
-val read = read_pos Position.none;
+val read_text = reader {opaque_warning = true} scan_ml_antiq o Symbol_Pos.explode;
+fun read text = read_text (text, Position.none);
fun read_set_range range =
read #> map (fn Antiquote.Text tok => Antiquote.Text (set_range range tok) | antiq => antiq);
-fun read_source SML source =
+fun read_source' {language, symbols, opaque_warning} scan source =
let
val pos = Input.pos_of source;
- val language = if SML then Markup.language_SML else Markup.language_ML;
val _ =
if Position.is_reported_range pos
then Position.report pos (language (Input.is_delimited source))
else ();
- in gen_read SML pos (Input.text_of source) end;
+ val syms =
+ Symbol_Pos.explode (Input.text_of source, pos)
+ |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p));
+ in reader {opaque_warning = opaque_warning} scan syms end;
+
+val read_source =
+ read_source' {language = Markup.language_ML, symbols = true, opaque_warning = true}
+ scan_ml_antiq;
+
+val read_source_sml =
+ read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false}
+ scan_sml_antiq;
end;
--- a/src/Pure/Thy/document_antiquotations.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Mon Aug 27 20:43:01 2018 +0200
@@ -264,7 +264,7 @@
in Input.source_content text end);
fun ml_enclose bg en source =
- ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;
+ ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;
in
--- a/src/Pure/Tools/debugger.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/Tools/debugger.ML Mon Aug 27 20:43:01 2018 +0200
@@ -131,18 +131,19 @@
"Context.put_generic_context (SOME (Context.Proof ML_context))",
"Context.put_generic_context (SOME ML_context)"];
-fun make_environment sml = if sml then ML_Env.SML else ML_Env.Isabelle;
+fun environment SML = if SML then ML_Env.SML else ML_Env.Isabelle;
+fun operations SML = if SML then ML_Env.SML_operations else ML_Env.Isabelle_operations;
fun evaluate {SML, verbose} =
ML_Context.eval
- {environment = make_environment SML, redirect = false, verbose = verbose,
+ {environment = environment SML, redirect = false, verbose = verbose,
debug = SOME false, writeln = writeln_message, warning = warning_message}
Position.none;
fun eval_setup thread_name index SML context =
context
|> Context_Position.set_visible_generic false
- |> ML_Env.add_name_space (make_environment SML)
+ |> ML_Env.add_name_space (environment SML)
(PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
fun eval_context thread_name index SML toks =
@@ -170,13 +171,13 @@
fun eval thread_name index SML txt1 txt2 =
let
- val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
+ val (toks1, toks2) = apply2 (#read_source (operations SML) o Input.string) (txt1, txt2);
val context = eval_context thread_name index SML toks1;
in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
fun print_vals thread_name index SML txt =
let
- val toks = ML_Lex.read_source SML (Input.string txt)
+ val toks = #read_source (operations SML) (Input.string txt)
val context = eval_context thread_name index SML toks;
val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);