clarified check_thy_reader: check node_name here;
authorwenzelm
Sat Jan 07 20:44:37 2017 +0100 (2017-01-07)
changeset 64826c97296294f6d
parent 64825 e78b62c289bb
child 64827 4ef1eb75f1cd
clarified check_thy_reader: check node_name here;
src/Pure/PIDE/resources.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/jEdit/src/document_model.scala
     1.1 --- a/src/Pure/PIDE/resources.scala	Sat Jan 07 20:37:48 2017 +0100
     1.2 +++ b/src/Pure/PIDE/resources.scala	Sat Jan 07 20:44:37 2017 +0100
     1.3 @@ -121,7 +121,7 @@
     1.4        reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true)
     1.5      : Document.Node.Header =
     1.6    {
     1.7 -    if (reader.source.length > 0) {
     1.8 +    if (node_name.is_theory && reader.source.length > 0) {
     1.9        try {
    1.10          val header = Thy_Header.read(reader, start, strict).decode_symbols
    1.11  
     2.1 --- a/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 20:37:48 2017 +0100
     2.2 +++ b/src/Tools/VSCode/src/document_model.scala	Sat Jan 07 20:44:37 2017 +0100
     2.3 @@ -43,11 +43,7 @@
     2.4  
     2.5    def node_header: Document.Node.Header =
     2.6      resources.special_header(node_name) getOrElse
     2.7 -    {
     2.8 -      if (is_theory)
     2.9 -        resources.check_thy_reader("", node_name, Scan.char_reader(doc.text))
    2.10 -      else Document.Node.no_header
    2.11 -    }
    2.12 +      resources.check_thy_reader("", node_name, Scan.char_reader(doc.text))
    2.13  
    2.14  
    2.15    /* perspective */
     3.1 --- a/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 20:37:48 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sat Jan 07 20:44:37 2017 +0100
     3.3 @@ -238,12 +238,7 @@
     3.4  
     3.5    def node_header: Document.Node.Header =
     3.6      PIDE.resources.special_header(node_name) getOrElse
     3.7 -    {
     3.8 -      if (is_theory)
     3.9 -        PIDE.resources.check_thy_reader(
    3.10 -          "", node_name, Scan.char_reader(content.text), strict = false)
    3.11 -      else Document.Node.no_header
    3.12 -    }
    3.13 +      PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false)
    3.14  
    3.15  
    3.16    /* content */
    3.17 @@ -305,15 +300,10 @@
    3.18      GUI_Thread.require {}
    3.19  
    3.20      PIDE.resources.special_header(node_name) getOrElse
    3.21 -    {
    3.22 -      if (is_theory) {
    3.23 -        JEdit_Lib.buffer_lock(buffer) {
    3.24 -          PIDE.resources.check_thy_reader(
    3.25 -            "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
    3.26 -        }
    3.27 +      JEdit_Lib.buffer_lock(buffer) {
    3.28 +        PIDE.resources.check_thy_reader(
    3.29 +          "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
    3.30        }
    3.31 -      else Document.Node.no_header
    3.32 -    }
    3.33    }
    3.34  
    3.35