# HG changeset patch
# User wenzelm
# Date 1535395381 -7200
# Node ID 5e7b1ae10eb8d554204f5825418fb3d9319d6281
# Parent  253f04c1e8146a684ec6fd1616facbef7cfc1162
clarified signature;

diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Doc/antiquote_setup.ML
--- 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)))
diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/HOL/ex/Cartouche_Examples.thy
--- 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>
diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Pure/Isar/attrib.ML
--- 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 ^ ")")
diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Pure/Isar/isar_cmd.ML
--- 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 " ^
diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Pure/Isar/method.ML
--- 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) ^
diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Pure/ML/ml_context.ML
--- 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
diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Pure/ML/ml_env.ML
--- 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);
 
diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Pure/ML/ml_lex.ML
--- 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;
 
diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Pure/Thy/document_antiquotations.ML
--- 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
 
diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Pure/Tools/debugger.ML
--- 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);