# HG changeset patch
# User wenzelm
# Date 1417611878 -3600
# Node ID 88b0b1f28adc4bd4c768b91b3f1953ad5a62f267
# Parent  25501ba956acb8af38f2d556cb812a5d99e741d0
tuned signature;

diff -r 25501ba956ac -r 88b0b1f28adc src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -204,7 +204,7 @@
     Keyword.is_command keywords name andalso
       let
         val markup =
-          Outer_Syntax.scan keywords Position.none name
+          Token.explode keywords Position.none name
           |> maps (Outer_Syntax.command_reports thy)
           |> map (snd o fst);
         val _ = Context_Position.reports ctxt (map (pair pos) markup);
diff -r 25501ba956ac -r 88b0b1f28adc src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -534,8 +534,8 @@
   let
     fun do_method named_thms ctxt =
       let
-        val ref_of_str =
-          suffix ";" #> Outer_Syntax.scan (Thy_Header.get_keywords' ctxt) Position.none
+        val ref_of_str = (* FIXME proper wrapper for parser combinators *)
+          suffix ";" #> Token.explode (Thy_Header.get_keywords' ctxt) Position.none
           #> Parse.xthm #> fst
         val thms = named_thms |> maps snd
         val facts = named_thms |> map (ref_of_str o fst o fst)
@@ -561,7 +561,7 @@
           let
             val (type_encs, lam_trans) =
               !meth
-              |> Outer_Syntax.scan (Thy_Header.get_keywords' ctxt) Position.start
+              |> Token.explode (Thy_Header.get_keywords' ctxt) Position.start
               |> filter Token.is_proper |> tl
               |> Metis_Tactic.parse_metis_options |> fst
               |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
diff -r 25501ba956ac -r 88b0b1f28adc src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -221,7 +221,7 @@
 
     val thy = Proof_Context.theory_of lthy
     val dummy_thm = Thm.transfer thy Drule.dummy_thm
-    val pointer = Outer_Syntax.scan (Thy_Header.get_keywords thy) Position.none bundle_name
+    val pointer = Token.explode (Thy_Header.get_keywords thy) Position.none bundle_name
     val restore_lifting_att = 
       ([dummy_thm], [Token.src ("Lifting.lifting_restore_internal", Position.none) pointer])
   in
diff -r 25501ba956ac -r 88b0b1f28adc src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -43,7 +43,7 @@
 
 fun parse_method keywords s =
   enclose "(" ")" s
-  |> Outer_Syntax.scan keywords Position.start
+  |> Token.explode keywords Position.start
   |> filter Token.is_proper
   |> Scan.read Token.stopper Method.parse
   |> (fn SOME (Method.Source src, _) => src | _ => raise Fail "expected Source");
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -19,7 +19,6 @@
     (bool -> local_theory -> Proof.state) parser -> unit
   val local_theory_to_proof: command_spec -> string ->
     (local_theory -> Proof.state) parser -> unit
-  val scan: Keyword.keywords -> Position.T -> string -> Token.T list
   val parse: theory -> Position.T -> string -> Toplevel.transition list
   val parse_tokens: theory -> Token.T list -> Toplevel.transition list
   val parse_spans: Token.T list -> Command_Span.span list
@@ -148,15 +147,6 @@
 
 (** toplevel parsing **)
 
-(* scan tokens *)
-
-fun scan keywords pos =
-  Source.of_string #>
-  Symbol.source #>
-  Token.source keywords pos #>
-  Source.exhaust;
-
-
 (* parse commands *)
 
 local
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Dec 03 14:04:38 2014 +0100
@@ -7,7 +7,6 @@
 package isabelle
 
 
-import scala.util.parsing.input.{Reader, CharSequenceReader}
 import scala.collection.mutable
 import scala.annotation.tailrec
 
@@ -184,33 +183,6 @@
   }
 
 
-  /* token language */
-
-  def scan(input: CharSequence): List[Token] =
-  {
-    val in: Reader[Char] = new CharSequenceReader(input)
-    Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(keywords)), in) match {
-      case Token.Parsers.Success(tokens, _) => tokens
-      case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
-    }
-  }
-
-  def scan_line(input: CharSequence, context: Scan.Line_Context): (List[Token], Scan.Line_Context) =
-  {
-    var in: Reader[Char] = new CharSequenceReader(input)
-    val toks = new mutable.ListBuffer[Token]
-    var ctxt = context
-    while (!in.atEnd) {
-      Token.Parsers.parse(Token.Parsers.token_line(keywords, ctxt), in) match {
-        case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
-        case Token.Parsers.NoSuccess(_, rest) =>
-          error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
-      }
-    }
-    (toks.toList, ctxt)
-  }
-
-
   /* command spans */
 
   def parse_spans(toks: List[Token]): List[Command_Span.Span] =
@@ -249,7 +221,7 @@
   }
 
   def parse_spans(input: CharSequence): List[Command_Span.Span] =
-    parse_spans(scan(input))
+    parse_spans(Token.explode(keywords, input))
 
 
   /* overall document structure */
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -89,6 +89,7 @@
   val source_strict: Keyword.keywords ->
     Position.T -> (Symbol.symbol, 'a) Source.source -> (T,
       (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source
+  val explode: Keyword.keywords -> Position.T -> string -> T list
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
   val read_no_commands: Keyword.keywords -> 'a parser -> Symbol_Pos.T list -> 'a list
@@ -538,7 +539,7 @@
 fun token_range k (pos1, (ss, pos2)) =
   Token (Symbol_Pos.implode_range pos1 pos2 ss, (k, Symbol_Pos.content ss), Slot);
 
-fun scan keywords = !!! "bad input"
+fun scan_token keywords = !!! "bad input"
   (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
     Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
     scan_verbatim >> token_range Verbatim ||
@@ -571,7 +572,7 @@
 
 fun source' strict keywords =
   let
-    val scan_strict = Scan.bulk (scan keywords);
+    val scan_strict = Scan.bulk (scan_token keywords);
     val scan = if strict then scan_strict else Scan.recover scan_strict recover;
   in Source.source Symbol_Pos.stopper scan end;
 
@@ -581,6 +582,15 @@
 end;
 
 
+(* explode *)
+
+fun explode keywords pos =
+  Source.of_string #>
+  Symbol.source #>
+  source keywords pos #>
+  Source.exhaust;
+
+
 
 (** parsers **)
 
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Isar/token.scala	Wed Dec 03 14:04:38 2014 +0100
@@ -7,6 +7,10 @@
 package isabelle
 
 
+import scala.collection.mutable
+import scala.util.parsing.input
+
+
 object Token
 {
   /* tokens */
@@ -121,6 +125,34 @@
   }
 
 
+  /* explode */
+
+  def explode(keywords: Keyword.Keywords, inp: CharSequence): List[Token] =
+  {
+    val in: input.Reader[Char] = new input.CharSequenceReader(inp)
+    Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), in) match {
+      case Parsers.Success(tokens, _) => tokens
+      case _ => error("Unexpected failure of tokenizing input:\n" + inp.toString)
+    }
+  }
+
+  def explode_line(keywords: Keyword.Keywords, inp: CharSequence, context: Scan.Line_Context)
+    : (List[Token], Scan.Line_Context) =
+  {
+    var in: input.Reader[Char] = new input.CharSequenceReader(inp)
+    val toks = new mutable.ListBuffer[Token]
+    var ctxt = context
+    while (!in.atEnd) {
+      Parsers.parse(Parsers.token_line(keywords, ctxt), in) match {
+        case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
+        case Parsers.NoSuccess(_, rest) =>
+          error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
+      }
+    }
+    (toks.toList, ctxt)
+  }
+
+
   /* token reader */
 
   object Pos
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -333,7 +333,7 @@
       val span =
         Lazy.lazy (fn () =>
           Position.setmp_thread_data (Position.id_only id)
-            (fn () => Outer_Syntax.scan (get_keywords ()) (Position.id id) text) ());
+            (fn () => Token.explode (get_keywords ()) (Position.id id) text) ());
       val _ =
         Position.setmp_thread_data (Position.id_only id)
           (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -151,7 +151,7 @@
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
 
-    val toks = Outer_Syntax.scan keywords text_pos text;
+    val toks = Token.explode keywords text_pos text;
     val spans = Outer_Syntax.parse_spans toks;
     val elements = Thy_Syntax.parse_elements keywords spans;
 
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/System/options.scala	Wed Dec 03 14:04:38 2014 +0100
@@ -108,7 +108,7 @@
     def parse_file(syntax: Outer_Syntax, parser: Parser[Options => Options],
       options: Options, file: Path): Options =
     {
-      val toks = syntax.scan(File.read(file))
+      val toks = Token.explode(syntax.keywords, File.read(file))
       val ops =
         parse_all(rep(parser), Token.reader(toks, file.implode)) match {
           case Success(result, _) => result
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Tools/build.scala	Wed Dec 03 14:04:38 2014 +0100
@@ -259,7 +259,7 @@
 
     def parse_entries(root: Path): List[(String, Session_Entry)] =
     {
-      val toks = root_syntax.scan(File.read(root))
+      val toks = Token.explode(root_syntax.keywords, File.read(root))
 
       parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match {
         case Success(result, _) =>
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Tools/find_consts.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -145,7 +145,7 @@
 in
 
 fun read_query pos str =
-  Outer_Syntax.scan query_keywords pos str
+  Token.explode query_keywords pos str
   |> filter Token.is_proper
   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   |> #1;
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -531,7 +531,7 @@
 in
 
 fun read_query pos str =
-  Outer_Syntax.scan query_keywords pos str
+  Token.explode query_keywords pos str
   |> filter Token.is_proper
   |> Scan.error (Scan.finite Token.stopper (Parse.!!! (query --| Scan.ahead Parse.eof)))
   |> #1;
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Tools/update_cartouches.scala
--- a/src/Pure/Tools/update_cartouches.scala	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Tools/update_cartouches.scala	Wed Dec 03 14:04:38 2014 +0100
@@ -20,7 +20,7 @@
   {
     val text0 = File.read(path)
     val text1 =
-      (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
+      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
         yield {
           if (tok.kind == Token.Kind.ALT_STRING) cartouche(tok.content)
           else if (tok.kind == Token.Kind.VERBATIM) {
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Tools/update_header.scala
--- a/src/Pure/Tools/update_header.scala	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Tools/update_header.scala	Wed Dec 03 14:04:38 2014 +0100
@@ -13,7 +13,7 @@
   {
     val text0 = File.read(path)
     val text1 =
-      (for (tok <- Outer_Syntax.empty.scan(text0).iterator)
+      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator)
         yield { if (tok.source == "header") section else tok.source }).mkString
 
     if (text0 != text1) {
diff -r 25501ba956ac -r 88b0b1f28adc src/Pure/Tools/update_semicolons.scala
--- a/src/Pure/Tools/update_semicolons.scala	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Pure/Tools/update_semicolons.scala	Wed Dec 03 14:04:38 2014 +0100
@@ -13,7 +13,7 @@
   {
     val text0 = File.read(path)
     val text1 =
-      (for (tok <- Outer_Syntax.empty.scan(text0).iterator if tok.source != ";")
+      (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator if tok.source != ";")
         yield tok.source).mkString
 
     if (text0 != text1) {
diff -r 25501ba956ac -r 88b0b1f28adc src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Wed Dec 03 14:04:38 2014 +0100
@@ -696,7 +696,7 @@
     val thy = Thy_Info.get_theory thyname;
     val ctxt = Proof_Context.init_global thy;
     val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o
-      (filter Token.is_proper o Outer_Syntax.scan (Thy_Header.get_keywords thy) Position.none);
+      (filter Token.is_proper o Token.explode (Thy_Header.get_keywords thy) Position.none);
   in case parse cmd_expr
    of SOME f => (writeln "Now generating code..."; f ctxt)
     | NONE => error ("Bad directive " ^ quote cmd_expr)
diff -r 25501ba956ac -r 88b0b1f28adc src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Wed Dec 03 11:50:58 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Wed Dec 03 14:04:38 2014 +0100
@@ -218,7 +218,7 @@
     for {
       ctxt <- line_context.context
       text <- JEdit_Lib.try_get_text(buffer, JEdit_Lib.line_range(buffer, line))
-    } yield syntax.scan_line(text, ctxt)._1
+    } yield Token.explode_line(syntax.keywords, text, ctxt)._1
   }
 
   def line_token_iterator(
@@ -346,7 +346,7 @@
               (styled_tokens, new Line_Context(Some(ctxt1), structure))
 
             case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
-              val (tokens, ctxt1) = syntax.scan_line(line, ctxt)
+              val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
               val structure1 = syntax.line_structure(tokens, structure)
               val styled_tokens =
                 tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))