--- 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 }