more uniform node_header (non-strict);
authorwenzelm
Sat Jan 07 20:37:48 2017 +0100 (2017-01-07)
changeset 64825e78b62c289bb
parent 64824 330ec9bc4b75
child 64826 c97296294f6d
more uniform node_header (non-strict);
removed dead code;
src/Pure/PIDE/command.scala
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_header.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Sat Jan 07 20:01:05 2017 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Jan 07 20:37:48 2017 +0100
     1.3 @@ -349,8 +349,8 @@
     1.4      span.name match {
     1.5        // inlined errors
     1.6        case Thy_Header.THEORY =>
     1.7 -        val header =
     1.8 -          resources.check_thy_reader("", node_name, Scan.char_reader(Token.implode(span.content)))
     1.9 +        val reader = Scan.char_reader(Token.implode(span.content))
    1.10 +        val header = resources.check_thy_reader("", node_name, reader)
    1.11          val errors =
    1.12            for ((imp, pos) <- header.imports if !can_import(imp)) yield {
    1.13              val msg =
     2.1 --- a/src/Pure/PIDE/resources.scala	Sat Jan 07 20:01:05 2017 +0100
     2.2 +++ b/src/Pure/PIDE/resources.scala	Sat Jan 07 20:37:48 2017 +0100
     2.3 @@ -118,11 +118,12 @@
     2.4    }
     2.5  
     2.6    def check_thy_reader(qualifier: String, node_name: Document.Node.Name,
     2.7 -    reader: Reader[Char], start: Token.Pos = Token.Pos.command): Document.Node.Header =
     2.8 +      reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
     2.9 +    : Document.Node.Header =
    2.10    {
    2.11      if (reader.source.length > 0) {
    2.12        try {
    2.13 -        val header = Thy_Header.read(reader, start).decode_symbols
    2.14 +        val header = Thy_Header.read(reader, start, strict).decode_symbols
    2.15  
    2.16          val base_name = Long_Name.base_name(node_name.theory)
    2.17          val (name, pos) = header.name
    2.18 @@ -140,9 +141,9 @@
    2.19      else Document.Node.no_header
    2.20    }
    2.21  
    2.22 -  def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos = Token.Pos.command)
    2.23 -    : Document.Node.Header =
    2.24 -    with_thy_reader(name, check_thy_reader(qualifier, name, _, start))
    2.25 +  def check_thy(qualifier: String, name: Document.Node.Name,
    2.26 +      start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header =
    2.27 +    with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict))
    2.28  
    2.29    def check_file(file: String): Boolean =
    2.30      try {
     3.1 --- a/src/Pure/Thy/thy_header.scala	Sat Jan 07 20:01:05 2017 +0100
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Jan 07 20:37:48 2017 +0100
     3.3 @@ -154,56 +154,27 @@
     3.4  
     3.5    /* read -- lazy scanning */
     3.6  
     3.7 -  def read(reader: Reader[Char], start: Token.Pos): Thy_Header =
     3.8 +  def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
     3.9    {
    3.10      val token = Token.Parsers.token(bootstrap_keywords)
    3.11 -    val toks = new mutable.ListBuffer[Token]
    3.12 -
    3.13 -    @tailrec def scan_to_begin(in: Reader[Char])
    3.14 -    {
    3.15 +    def make_tokens(in: Reader[Char]): Stream[Token] =
    3.16        token(in) match {
    3.17 -        case Token.Parsers.Success(tok, rest) =>
    3.18 -          toks += tok
    3.19 -          if (!tok.is_begin) scan_to_begin(rest)
    3.20 -        case _ =>
    3.21 +        case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest)
    3.22 +        case _ => Stream.empty
    3.23        }
    3.24 -    }
    3.25 -    scan_to_begin(reader)
    3.26 +
    3.27 +    val tokens =
    3.28 +      if (strict) make_tokens(reader)
    3.29 +      else make_tokens(reader).dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
    3.30  
    3.31 -    parse(commit(header), Token.reader(toks.toList, start)) match {
    3.32 +    val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList
    3.33 +    val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList
    3.34 +
    3.35 +    parse(commit(header), Token.reader(tokens1 ::: tokens2, start)) match {
    3.36        case Success(result, _) => result
    3.37        case bad => error(bad.toString)
    3.38      }
    3.39    }
    3.40 -
    3.41 -
    3.42 -  /* line-oriented text */
    3.43 -
    3.44 -  def header_text(doc: Line.Document): String =
    3.45 -  {
    3.46 -    val keywords = bootstrap_syntax.keywords
    3.47 -    val toks = new mutable.ListBuffer[Token]
    3.48 -    val iterator =
    3.49 -      (for {
    3.50 -        (toks, _) <-
    3.51 -          doc.lines.iterator.scanLeft((List.empty[Token], Scan.Finished: Scan.Line_Context))(
    3.52 -            {
    3.53 -              case ((_, ctxt), line) => Token.explode_line(keywords, line.text, ctxt)
    3.54 -            })
    3.55 -        tok <- toks.iterator ++ Iterator.single(Token.newline)
    3.56 -      } yield tok).dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
    3.57 -
    3.58 -    @tailrec def until_begin
    3.59 -    {
    3.60 -      if (iterator.hasNext) {
    3.61 -        val tok = iterator.next
    3.62 -        toks += tok
    3.63 -        if (!tok.is_begin) until_begin
    3.64 -      }
    3.65 -    }
    3.66 -    until_begin
    3.67 -    Token.implode(toks.toList)
    3.68 -  }
    3.69  }
    3.70  
    3.71  
     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 20:01:05 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 20:37:48 2017 +0100
     4.3 @@ -236,12 +236,12 @@
     4.4  {
     4.5    /* header */
     4.6  
     4.7 -  // FIXME eliminate clone
     4.8    def node_header: Document.Node.Header =
     4.9      PIDE.resources.special_header(node_name) getOrElse
    4.10      {
    4.11        if (is_theory)
    4.12 -        PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text))
    4.13 +        PIDE.resources.check_thy_reader(
    4.14 +          "", node_name, Scan.char_reader(content.text), strict = false)
    4.15        else Document.Node.no_header
    4.16      }
    4.17  
    4.18 @@ -304,24 +304,12 @@
    4.19    {
    4.20      GUI_Thread.require {}
    4.21  
    4.22 -    // FIXME eliminate clone
    4.23      PIDE.resources.special_header(node_name) getOrElse
    4.24      {
    4.25        if (is_theory) {
    4.26          JEdit_Lib.buffer_lock(buffer) {
    4.27 -          Token_Markup.line_token_iterator(
    4.28 -            Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
    4.29 -              {
    4.30 -                case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start
    4.31 -              })
    4.32 -            match {
    4.33 -              case Some(offset) =>
    4.34 -                val length = buffer.getLength - offset
    4.35 -                PIDE.resources.check_thy_reader("", node_name,
    4.36 -                  Scan.char_reader(buffer.getSegment(offset, length)))
    4.37 -              case None =>
    4.38 -                Document.Node.no_header
    4.39 -            }
    4.40 +          PIDE.resources.check_thy_reader(
    4.41 +            "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
    4.42          }
    4.43        }
    4.44        else Document.Node.no_header