# HG changeset patch
# User wenzelm
# Date 1407795422 -7200
# Node ID 020df63dd0a95f40c957f4946b047ce43f5bc6b7
# Parent  c0c5652e796e0d105a9c67aef6ce3e3b3e9f4402
tuned signature;

diff -r c0c5652e796e -r 020df63dd0a9 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:17:02 2014 +0200
@@ -186,6 +186,9 @@
     result.toList
   }
 
+  def parse_spans(input: CharSequence): List[Command_Span.Span] =
+    parse_spans(scan(input))
+
 
   /* language context */
 
diff -r c0c5652e796e -r 020df63dd0a9 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Tue Aug 12 00:08:32 2014 +0200
+++ b/src/Pure/PIDE/prover.scala	Tue Aug 12 00:17:02 2014 +0200
@@ -14,8 +14,7 @@
   trait Syntax
   {
     def add_keywords(keywords: Thy_Header.Keywords): Syntax
-    def scan(input: CharSequence): List[Token]
-    def parse_spans(toks: List[Token]): List[Command_Span.Span]
+    def parse_spans(input: CharSequence): List[Command_Span.Span]
     def load_command(name: String): Option[List[String]]
     def load_commands_in(text: String): Boolean
   }
diff -r c0c5652e796e -r 020df63dd0a9 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Aug 12 00:08:32 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Aug 12 00:17:02 2014 +0200
@@ -56,7 +56,7 @@
 
   def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
     if (syntax.load_commands_in(text)) {
-      val spans = syntax.parse_spans(syntax.scan(text))
+      val spans = syntax.parse_spans(text)
       spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
     }
     else Nil
diff -r c0c5652e796e -r 020df63dd0a9 src/Pure/Thy/thy_structure.scala
--- a/src/Pure/Thy/thy_structure.scala	Tue Aug 12 00:08:32 2014 +0200
+++ b/src/Pure/Thy/thy_structure.scala	Tue Aug 12 00:17:02 2014 +0200
@@ -63,7 +63,7 @@
 
     /* result structure */
 
-    val spans = syntax.parse_spans(syntax.scan(text))
+    val spans = syntax.parse_spans(text)
     spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
     result()
   }
diff -r c0c5652e796e -r 020df63dd0a9 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 00:17:02 2014 +0200
@@ -168,7 +168,7 @@
   {
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
-      syntax.parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
+      syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
         map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
 
     val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)