tuned signature;
authorwenzelm
Tue Aug 12 00:17:02 2014 +0200 (2014-08-12)
changeset 57906020df63dd0a9
parent 57905 c0c5652e796e
child 57907 7fc36b4c7cce
tuned signature;
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_structure.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 12 00:17:02 2014 +0200
     1.3 @@ -186,6 +186,9 @@
     1.4      result.toList
     1.5    }
     1.6  
     1.7 +  def parse_spans(input: CharSequence): List[Command_Span.Span] =
     1.8 +    parse_spans(scan(input))
     1.9 +
    1.10  
    1.11    /* language context */
    1.12  
     2.1 --- a/src/Pure/PIDE/prover.scala	Tue Aug 12 00:08:32 2014 +0200
     2.2 +++ b/src/Pure/PIDE/prover.scala	Tue Aug 12 00:17:02 2014 +0200
     2.3 @@ -14,8 +14,7 @@
     2.4    trait Syntax
     2.5    {
     2.6      def add_keywords(keywords: Thy_Header.Keywords): Syntax
     2.7 -    def scan(input: CharSequence): List[Token]
     2.8 -    def parse_spans(toks: List[Token]): List[Command_Span.Span]
     2.9 +    def parse_spans(input: CharSequence): List[Command_Span.Span]
    2.10      def load_command(name: String): Option[List[String]]
    2.11      def load_commands_in(text: String): Boolean
    2.12    }
     3.1 --- a/src/Pure/PIDE/resources.scala	Tue Aug 12 00:08:32 2014 +0200
     3.2 +++ b/src/Pure/PIDE/resources.scala	Tue Aug 12 00:17:02 2014 +0200
     3.3 @@ -56,7 +56,7 @@
     3.4  
     3.5    def loaded_files(syntax: Prover.Syntax, text: String): List[String] =
     3.6      if (syntax.load_commands_in(text)) {
     3.7 -      val spans = syntax.parse_spans(syntax.scan(text))
     3.8 +      val spans = syntax.parse_spans(text)
     3.9        spans.iterator.map(Command_Span.span_files(syntax, _)).flatten.toList
    3.10      }
    3.11      else Nil
     4.1 --- a/src/Pure/Thy/thy_structure.scala	Tue Aug 12 00:08:32 2014 +0200
     4.2 +++ b/src/Pure/Thy/thy_structure.scala	Tue Aug 12 00:17:02 2014 +0200
     4.3 @@ -63,7 +63,7 @@
     4.4  
     4.5      /* result structure */
     4.6  
     4.7 -    val spans = syntax.parse_spans(syntax.scan(text))
     4.8 +    val spans = syntax.parse_spans(text)
     4.9      spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
    4.10      result()
    4.11    }
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 00:08:32 2014 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 12 00:17:02 2014 +0200
     5.3 @@ -168,7 +168,7 @@
     5.4    {
     5.5      val cmds0 = commands.iterator(first, last).toList
     5.6      val blobs_spans0 =
     5.7 -      syntax.parse_spans(syntax.scan(cmds0.iterator.map(_.source).mkString)).
     5.8 +      syntax.parse_spans(cmds0.iterator.map(_.source).mkString).
     5.9          map(span => (Command_Span.resolve_files(resources, syntax, name, span, get_blob), span))
    5.10  
    5.11      val (cmds1, blobs_spans1) = chop_common(cmds0, blobs_spans0)