tight span for theory header, which is relevant for error positions (including semantic completion);
authorwenzelm
Tue Mar 17 16:17:49 2015 +0100 (2015-03-17)
changeset 597365c1a0069b9d3
parent 59735 24bee1b11fce
child 59737 c443ca40ef8d
tight span for theory header, which is relevant for error positions (including semantic completion);
src/Pure/Thy/thy_header.scala
src/Pure/Tools/build.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/Thy/thy_header.scala	Tue Mar 17 15:21:41 2015 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Mar 17 16:17:49 2015 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4    private val bootstrap_keywords =
     1.5      Keyword.Keywords.empty.add_keywords(bootstrap_header)
     1.6  
     1.7 -  def bootstrap_syntax(): Outer_Syntax =
     1.8 +  lazy val bootstrap_syntax: Outer_Syntax =
     1.9      Outer_Syntax.init().add_keywords(bootstrap_header)
    1.10  
    1.11  
     2.1 --- a/src/Pure/Tools/build.scala	Tue Mar 17 15:21:41 2015 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 17 16:17:49 2015 +0100
     2.3 @@ -438,7 +438,7 @@
     2.4                info.parent.map(deps(_)) match {
     2.5                  case None =>
     2.6                    (Set.empty[String], Map.empty[String, Document.Node.Name],
     2.7 -                    Thy_Header.bootstrap_syntax())
     2.8 +                    Thy_Header.bootstrap_syntax)
     2.9                  case Some(parent) =>
    2.10                    (parent.loaded_theories, parent.known_theories, parent.syntax)
    2.11                }
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 17 15:21:41 2015 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 17 16:17:49 2015 +0100
     3.3 @@ -12,6 +12,7 @@
     3.4  import isabelle._
     3.5  
     3.6  import scala.collection.mutable
     3.7 +import scala.util.parsing.input.CharSequenceReader
     3.8  
     3.9  import org.gjt.sp.jedit.jEdit
    3.10  import org.gjt.sp.jedit.Buffer
    3.11 @@ -78,13 +79,17 @@
    3.12  
    3.13      if (is_theory) {
    3.14        JEdit_Lib.buffer_lock(buffer) {
    3.15 -        Exn.capture {
    3.16 +        val toks1 =
    3.17 +          Token_Markup.line_token_iterator(
    3.18 +            Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).map(_.info).
    3.19 +            takeWhile(tok => !tok.is_begin).toList
    3.20 +        val toks =
    3.21 +          toks1.dropWhile(tok => !(tok.is_command && tok.source == Thy_Header.THEORY)) :::
    3.22 +            List(Token(Token.Kind.KEYWORD, "begin"))
    3.23 +        if (toks.nonEmpty)
    3.24            PIDE.resources.check_thy_reader("", node_name,
    3.25 -            JEdit_Lib.buffer_reader(buffer), Token.Pos.command)
    3.26 -        } match {
    3.27 -          case Exn.Res(header) => header
    3.28 -          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
    3.29 -        }
    3.30 +            new CharSequenceReader(Token.implode(toks)), Token.Pos.command)
    3.31 +        else Document.Node.no_header
    3.32        }
    3.33      }
    3.34      else Document.Node.no_header