--- 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" +
--- 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)
}
--- 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
{
--- 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) {
--- 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 =
--- 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 */
--- 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) {
--- 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
}
--- 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 }
--- 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
}
--- 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 =
{