# HG changeset patch
# User wenzelm
# Date 1483817868 -3600
# Node ID e78b62c289bb77916c58baa338b104e38e74e9a3
# Parent  330ec9bc4b75bc1ec2c1bf4807712087cdf38451
more uniform node_header (non-strict);
removed dead code;

diff -r 330ec9bc4b75 -r e78b62c289bb src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Sat Jan 07 20:01:05 2017 +0100
+++ b/src/Pure/PIDE/command.scala	Sat Jan 07 20:37:48 2017 +0100
@@ -349,8 +349,8 @@
     span.name match {
       // inlined errors
       case Thy_Header.THEORY =>
-        val header =
-          resources.check_thy_reader("", node_name, Scan.char_reader(Token.implode(span.content)))
+        val reader = Scan.char_reader(Token.implode(span.content))
+        val header = resources.check_thy_reader("", node_name, reader)
         val errors =
           for ((imp, pos) <- header.imports if !can_import(imp)) yield {
             val msg =
diff -r 330ec9bc4b75 -r e78b62c289bb src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Sat Jan 07 20:01:05 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Sat Jan 07 20:37:48 2017 +0100
@@ -118,11 +118,12 @@
   }
 
   def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
-    reader: Reader[Char], start: Token.Pos = Token.Pos.command): Document.Node.Header =
+      reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
+    : Document.Node.Header =
   {
     if (reader.source.length > 0) {
       try {
-        val header = Thy_Header.read(reader, start).decode_symbols
+        val header = Thy_Header.read(reader, start, strict).decode_symbols
 
         val base_name = Long_Name.base_name(node_name.theory)
         val (name, pos) = header.name
@@ -140,9 +141,9 @@
     else Document.Node.no_header
   }
 
-  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos = Token.Pos.command)
-    : Document.Node.Header =
-    with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
+  def check_thy(qualifier: String, name: Document.Node.Name,
+      start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
+    with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
 
   def check_file(file: String): Boolean =
     try {
diff -r 330ec9bc4b75 -r e78b62c289bb src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sat Jan 07 20:01:05 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sat Jan 07 20:37:48 2017 +0100
@@ -154,56 +154,27 @@
 
   /* read -- lazy scanning */
 
-  def read(reader: Reader[Char], start: Token.Pos): Thy_Header =
+  def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
   {
     val token = Token.Parsers.token(bootstrap_keywords)
-    val toks = new mutable.ListBuffer[Token]
-
-    @tailrec def scan_to_begin(in: Reader[Char])
-    {
+    def make_tokens(in: Reader[Char]): Stream[Token] =
       token(in) match {
-        case Token.Parsers.Success(tok, rest) =>
-          toks += tok
-          if (!tok.is_begin) scan_to_begin(rest)
-        case _ =>
+        case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
+        case _ => Stream.empty
       }
-    }
-    scan_to_begin(reader)
+
+    val tokens =
+      if (strict) make_tokens(reader)
+      else make_tokens(reader).dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
 
-    parse(commit(header), Token.reader(toks.toList, start)) match {
+    val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList
+    val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList
+
+    parse(commit(header), Token.reader(tokens1 ::: tokens2, start)) match {
       case Success(result, _) => result
       case bad => error(bad.toString)
     }
   }
-
-
-  /* line-oriented text */
-
-  def header_text(doc: Line.Document): String =
-  {
-    val keywords = bootstrap_syntax.keywords
-    val toks = new mutable.ListBuffer[Token]
-    val iterator =
-      (for {
-        (toks, _) <-
-          doc.lines.iterator.scanLeft((List.empty[Token], Scan.Finished: Scan.Line_Context))(
-            {
-              case ((_, ctxt), line) => Token.explode_line(keywords, line.text, ctxt)
-            })
-        tok <- toks.iterator ++ Iterator.single(Token.newline)
-      } yield tok).dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
-
-    @tailrec def until_begin
-    {
-      if (iterator.hasNext) {
-        val tok = iterator.next
-        toks += tok
-        if (!tok.is_begin) until_begin
-      }
-    }
-    until_begin
-    Token.implode(toks.toList)
-  }
 }
 
 
diff -r 330ec9bc4b75 -r e78b62c289bb src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 20:01:05 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 20:37:48 2017 +0100
@@ -236,12 +236,12 @@
 {
   /* header */
 
-  // FIXME eliminate clone
   def node_header: Document.Node.Header =
     PIDE.resources.special_header(node_name) getOrElse
     {
       if (is_theory)
-        PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text))
+        PIDE.resources.check_thy_reader(
+          "", node_name, Scan.char_reader(content.text), strict = false)
       else Document.Node.no_header
     }
 
@@ -304,24 +304,12 @@
   {
     GUI_Thread.require {}
 
-    // FIXME eliminate clone
     PIDE.resources.special_header(node_name) getOrElse
     {
       if (is_theory) {
         JEdit_Lib.buffer_lock(buffer) {
-          Token_Markup.line_token_iterator(
-            Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
-              {
-                case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start
-              })
-            match {
-              case Some(offset) =>
-                val length = buffer.getLength - offset
-                PIDE.resources.check_thy_reader("", node_name,
-                  Scan.char_reader(buffer.getSegment(offset, length)))
-              case None =>
-                Document.Node.no_header
-            }
+          PIDE.resources.check_thy_reader(
+            "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
         }
       }
       else Document.Node.no_header