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;