# HG changeset patch
# User wenzelm
# Date 1483815665 -3600
# Node ID 330ec9bc4b75bc1ec2c1bf4807712087cdf38451
# Parent  78df3d65a1cc518cf5f175364f6d8e91ee8472ee
tuned signature;

diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Pure/General/antiquote.scala
--- a/src/Pure/General/antiquote.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Pure/General/antiquote.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -7,9 +7,6 @@
 package isabelle
 
 
-import scala.util.parsing.input.CharSequenceReader
-
-
 object Antiquote
 {
   sealed abstract class Antiquote { def source: String }
@@ -50,7 +47,7 @@
 
   def read(input: CharSequence): List[Antiquote] =
   {
-    Parsers.parseAll(Parsers.rep(Parsers.antiquote), new CharSequenceReader(input)) match {
+    Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input)) match {
       case Parsers.Success(xs, _) => xs
       case Parsers.NoSuccess(_, next) =>
         error("Malformed quotation/antiquotation source" +
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Pure/General/scan.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -10,7 +10,8 @@
 import scala.annotation.tailrec
 import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
 import scala.collection.immutable.PagedSeq
-import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
+import scala.util.parsing.input.{OffsetPosition, Position => InputPosition,
+  Reader, CharSequenceReader}
 import scala.util.parsing.combinator.RegexParsers
 
 import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream}
@@ -489,4 +490,10 @@
     val stream_length = connection.getContentLength
     make_byte_reader(stream, stream_length)
   }
+
+
+  /* plain text reader */
+
+  def char_reader(text: CharSequence): CharSequenceReader =
+    new CharSequenceReader(text)
 }
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Pure/Isar/token.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -128,18 +128,15 @@
   /* 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 {
+    Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), Scan.char_reader(inp)) 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)
+    var in: input.Reader[Char] = Scan.char_reader(inp)
     val toks = new mutable.ListBuffer[Token]
     var ctxt = context
     while (!in.atEnd) {
@@ -180,7 +177,7 @@
       val offset: Symbol.Offset,
       val file: String,
       val id: String)
-    extends scala.util.parsing.input.Position
+    extends input.Position
   {
     def column = 0
     def lineContents = ""
@@ -210,7 +207,7 @@
     override def toString: String = Position.here(position(), delimited = false)
   }
 
-  abstract class Reader extends scala.util.parsing.input.Reader[Token]
+  abstract class Reader extends input.Reader[Token]
 
   private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader
   {
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Pure/ML/ml_lex.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -8,7 +8,7 @@
 
 
 import scala.collection.mutable
-import scala.util.parsing.input.{Reader, CharSequenceReader}
+import scala.util.parsing.input.Reader
 
 
 object ML_Lex
@@ -265,17 +265,15 @@
   /* tokenize */
 
   def tokenize(input: CharSequence): List[Token] =
-  {
-    Parsers.parseAll(Parsers.rep(Parsers.token), new CharSequenceReader(input)) match {
+    Parsers.parseAll(Parsers.rep(Parsers.token), Scan.char_reader(input)) match {
       case Parsers.Success(tokens, _) => tokens
       case _ => error("Unexpected failure of tokenizing input:\n" + input.toString)
     }
-  }
 
   def tokenize_line(SML: Boolean, input: CharSequence, context: Scan.Line_Context)
     : (List[Token], Scan.Line_Context) =
   {
-    var in: Reader[Char] = new CharSequenceReader(input)
+    var in: Reader[Char] = Scan.char_reader(input)
     val toks = new mutable.ListBuffer[Token]
     var ctxt = context
     while (!in.atEnd) {
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -10,7 +10,6 @@
 
 import scala.collection.mutable
 import scala.collection.immutable.SortedMap
-import scala.util.parsing.input.CharSequenceReader
 
 
 object Command
@@ -351,8 +350,7 @@
       // inlined errors
       case Thy_Header.THEORY =>
         val header =
-          resources.check_thy_reader(
-            "", node_name, new CharSequenceReader(Token.implode(span.content)))
+          resources.check_thy_reader("", node_name, Scan.char_reader(Token.implode(span.content)))
         val errors =
           for ((imp, pos) <- header.imports if !can_import(imp)) yield {
             val msg =
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -9,7 +9,7 @@
 
 import scala.annotation.tailrec
 import scala.collection.mutable
-import scala.util.parsing.input.{Reader, CharSequenceReader}
+import scala.util.parsing.input.Reader
 import scala.util.matching.Regex
 
 
@@ -176,9 +176,6 @@
     }
   }
 
-  def read(source: CharSequence, start: Token.Pos): Thy_Header =
-    read(new CharSequenceReader(source), start)
-
 
   /* line-oriented text */
 
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -8,8 +8,8 @@
 
 
 import scala.collection.mutable
-import scala.util.parsing.input.{Reader, CharSequenceReader}
 import scala.util.parsing.combinator.RegexParsers
+import scala.util.parsing.input.Reader
 
 
 object Bibtex
@@ -383,17 +383,14 @@
   /* parse */
 
   def parse(input: CharSequence): List[Chunk] =
-  {
-    val in: Reader[Char] = new CharSequenceReader(input)
-    Parsers.parseAll(Parsers.rep(Parsers.chunk), in) match {
+    Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match {
       case Parsers.Success(result, _) => result
       case _ => error("Unexpected failure to parse input:\n" + input.toString)
     }
-  }
 
   def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) =
   {
-    var in: Reader[Char] = new CharSequenceReader(input)
+    var in: Reader[Char] = Scan.char_reader(input)
     val chunks = new mutable.ListBuffer[Chunk]
     var ctxt = context
     while (!in.atEnd) {
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -11,8 +11,6 @@
 
 import java.io.{File => JFile}
 
-import scala.util.parsing.input.CharSequenceReader
-
 
 object Document_Model
 {
@@ -47,7 +45,7 @@
     resources.special_header(node_name) getOrElse
     {
       if (is_theory)
-        resources.check_thy_reader("", node_name, new CharSequenceReader(doc.text))
+        resources.check_thy_reader("", node_name, Scan.char_reader(doc.text))
       else Document.Node.no_header
     }
 
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -11,7 +11,7 @@
 
 import java.io.{File => JFile}
 
-import scala.util.parsing.input.{Reader, CharSequenceReader}
+import scala.util.parsing.input.Reader
 
 
 object VSCode_Resources
@@ -71,8 +71,7 @@
   {
     val file = node_file(name)
     get_model(file) match {
-      case Some(model) =>
-        f(new CharSequenceReader(model.doc.text))
+      case Some(model) => f(Scan.char_reader(model.doc.text))
       case None if file.isFile =>
         val reader = Scan.byte_reader(file)
         try { f(reader) } finally { reader.close }
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -12,7 +12,6 @@
 import isabelle._
 
 import scala.collection.mutable
-import scala.util.parsing.input.CharSequenceReader
 
 import org.gjt.sp.jedit.{jEdit, View}
 import org.gjt.sp.jedit.Buffer
@@ -242,7 +241,7 @@
     PIDE.resources.special_header(node_name) getOrElse
     {
       if (is_theory)
-        PIDE.resources.check_thy_reader("", node_name, new CharSequenceReader(content.text))
+        PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text))
       else Document.Node.no_header
     }
 
@@ -319,7 +318,7 @@
               case Some(offset) =>
                 val length = buffer.getLength - offset
                 PIDE.resources.check_thy_reader("", node_name,
-                  new CharSequenceReader(buffer.getSegment(offset, length)))
+                  Scan.char_reader(buffer.getSegment(offset, length)))
               case None =>
                 Document.Node.no_header
             }
diff -r 78df3d65a1cc -r 330ec9bc4b75 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Jan 07 19:36:40 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Jan 07 20:01:05 2017 +0100
@@ -99,7 +99,7 @@
     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
 
   def buffer_reader(buffer: JEditBuffer): CharSequenceReader =
-    new CharSequenceReader(buffer.getSegment(0, buffer.getLength))
+    Scan.char_reader(buffer.getSegment(0, buffer.getLength))
 
   def buffer_mode(buffer: JEditBuffer): String =
   {