more uniform treatment of file name vs. theory name and special header;
authorwenzelm
Mon Dec 26 15:31:13 2016 +0100 (2016-12-26)
changeset 64673b5965890e54d
parent 64672 d8e0619abb60
child 64674 ef0a5fd30f3b
child 64675 c557279d93f2
more uniform treatment of file name vs. theory name and special header;
src/Pure/PIDE/resources.scala
src/Pure/Thy/thy_header.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/server.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Dec 26 13:28:37 2016 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Dec 26 15:31:13 2016 +0100
     1.3 @@ -155,6 +155,16 @@
     1.4      catch { case ERROR(_) => false }
     1.5  
     1.6  
     1.7 +  /* special header */
     1.8 +
     1.9 +  def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
    1.10 +    if (Thy_Header.is_ml_root(name.theory))
    1.11 +      Some(Document.Node.Header(List((import_name("", name, Thy_Header.ML_BOOTSTRAP), Position.none))))
    1.12 +    else if (Thy_Header.is_bootstrap(name.theory))
    1.13 +      Some(Document.Node.Header(List((import_name("", name, Thy_Header.PURE), Position.none))))
    1.14 +    else None
    1.15 +
    1.16 +
    1.17    /* document changes */
    1.18  
    1.19    def parse_change(
     2.1 --- a/src/Pure/Thy/thy_header.scala	Mon Dec 26 13:28:37 2016 +0100
     2.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Dec 26 15:31:13 2016 +0100
     2.3 @@ -69,7 +69,7 @@
     2.4      Outer_Syntax.init().add_keywords(bootstrap_header)
     2.5  
     2.6  
     2.7 -  /* file name */
     2.8 +  /* file name vs. theory name */
     2.9  
    2.10    val PURE = "Pure"
    2.11    val ML_BOOTSTRAP = "ML_Bootstrap"
    2.12 @@ -94,6 +94,12 @@
    2.13        case _ => None
    2.14      }
    2.15  
    2.16 +  def is_ml_root(theory: String): Boolean =
    2.17 +    ml_roots.exists({ case (_, b) => b == theory })
    2.18 +
    2.19 +  def is_bootstrap(theory: String): Boolean =
    2.20 +    bootstrap_thys.exists({ case (_, b) => b == theory })
    2.21 +
    2.22  
    2.23    /* header */
    2.24  
     3.1 --- a/src/Tools/VSCode/src/document_model.scala	Mon Dec 26 13:28:37 2016 +0100
     3.2 +++ b/src/Tools/VSCode/src/document_model.scala	Mon Dec 26 15:31:13 2016 +0100
     3.3 @@ -20,11 +20,14 @@
     3.4  
     3.5    def is_theory: Boolean = node_name.is_theory
     3.6  
     3.7 -  lazy val node_header: Document.Node.Header =
     3.8 -    if (is_theory)
     3.9 -      session.resources.check_thy_reader(
    3.10 -        "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
    3.11 -    else Document.Node.no_header
    3.12 +  def node_header(resources: VSCode_Resources): Document.Node.Header =
    3.13 +    resources.special_header(node_name) getOrElse
    3.14 +    {
    3.15 +      if (is_theory)
    3.16 +        session.resources.check_thy_reader(
    3.17 +          "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
    3.18 +      else Document.Node.no_header
    3.19 +    }
    3.20  
    3.21  
    3.22    /* edits */
    3.23 @@ -32,9 +35,9 @@
    3.24    def text_edits: List[Text.Edit] =
    3.25      if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
    3.26  
    3.27 -  def node_edits: List[Document.Edit_Text] =
    3.28 +  def node_edits(resources: VSCode_Resources): List[Document.Edit_Text] =
    3.29      if (changed) {
    3.30 -      List(session.header_edit(node_name, node_header),
    3.31 +      List(session.header_edit(node_name, node_header(resources)),
    3.32          node_name -> Document.Node.Clear(),
    3.33          node_name -> Document.Node.Edits(text_edits),
    3.34          node_name ->
     4.1 --- a/src/Tools/VSCode/src/server.scala	Mon Dec 26 13:28:37 2016 +0100
     4.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Dec 26 15:31:13 2016 +0100
     4.3 @@ -200,7 +200,7 @@
     4.4          {
     4.5            val models = st.models
     4.6            val changed = (for { entry <- models.iterator if entry._2.changed } yield entry).toList
     4.7 -          val edits = for { (_, model) <- changed; edit <- model.node_edits } yield edit
     4.8 +          val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
     4.9            val models1 =
    4.10              (models /: changed)({ case (m, (uri, model)) => m + (uri -> model.unchanged) })
    4.11  
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 13:28:37 2016 +0100
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 26 15:31:13 2016 +0100
     5.3 @@ -73,25 +73,13 @@
     5.4  
     5.5    def is_theory: Boolean = node_name.is_theory
     5.6  
     5.7 -  def is_ml_root: Boolean =
     5.8 -    Thy_Header.ml_roots.exists({ case (_, name) => name == node_name.theory })
     5.9 -
    5.10 -  def is_bootstrap_thy: Boolean =
    5.11 -    Thy_Header.bootstrap_thys.exists({ case (_, name) => name == node_name.theory })
    5.12 -
    5.13    def node_header(): Document.Node.Header =
    5.14    {
    5.15      GUI_Thread.require {}
    5.16  
    5.17 -    if (is_ml_root)
    5.18 -      Document.Node.Header(
    5.19 -        List((PIDE.resources.import_name("", node_name, Thy_Header.ML_BOOTSTRAP), Position.none)))
    5.20 -    else if (is_theory) {
    5.21 -      if (is_bootstrap_thy) {
    5.22 -        Document.Node.Header(
    5.23 -          List((PIDE.resources.import_name("", node_name, Thy_Header.PURE), Position.none)))
    5.24 -      }
    5.25 -      else {
    5.26 +    PIDE.resources.special_header(node_name) getOrElse
    5.27 +    {
    5.28 +      if (is_theory) {
    5.29          JEdit_Lib.buffer_lock(buffer) {
    5.30            Token_Markup.line_token_iterator(
    5.31              Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
    5.32 @@ -103,12 +91,13 @@
    5.33                  val length = buffer.getLength - offset
    5.34                  PIDE.resources.check_thy_reader("", node_name,
    5.35                    new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command)
    5.36 -              case None => Document.Node.no_header
    5.37 +              case None =>
    5.38 +                Document.Node.no_header
    5.39              }
    5.40          }
    5.41        }
    5.42 +      else Document.Node.no_header
    5.43      }
    5.44 -    else Document.Node.no_header
    5.45    }
    5.46  
    5.47