# HG changeset patch
# User wenzelm
# Date 1406113290 -7200
# Node ID df1b3452d71cd2fa7f86fd1fa3cc54c462ddd7d7
# Parent  416ce9617780ba740bf59fcce55c08ceaff739db
more explicit discrimination of empty nodes -- suppress from Theories panel;

diff -r 416ce9617780 -r df1b3452d71c src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Jul 23 11:53:34 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Jul 23 13:01:30 2014 +0200
@@ -314,6 +314,8 @@
 
   sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
   {
+    def is_empty: Boolean = commands.isEmpty
+
     def same(that: Perspective): Boolean =
     {
       val cmds1 = this.commands
diff -r 416ce9617780 -r df1b3452d71c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Jul 23 11:53:34 2014 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Jul 23 13:01:30 2014 +0200
@@ -72,11 +72,23 @@
   visible_last = try List.last command_ids,
   overlays = Inttab.make_list overlays};
 
-val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["No theory header"]);
+val no_header = ("", Thy_Header.make ("", Position.none) [] [], []);
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
 
+fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
+  not required andalso
+  Inttab.is_empty visible andalso
+  is_none visible_last andalso
+  Inttab.is_empty overlays;
+
+fun is_empty_node (Node {header, perspective, entries, result}) =
+  header = no_header andalso
+  is_no_perspective perspective andalso
+  Entries.is_empty entries andalso
+  is_none result;
+
 
 (* basic components *)
 
diff -r 416ce9617780 -r df1b3452d71c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Jul 23 11:53:34 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Jul 23 13:01:30 2014 +0200
@@ -87,7 +87,7 @@
     sealed case class Header(
       imports: List[Name],
       keywords: Thy_Header.Keywords,
-      errors: List[String] = Nil)
+      errors: List[String])
     {
       def error(msg: String): Header = copy(errors = errors ::: List(msg))
 
@@ -95,10 +95,9 @@
         copy(errors = errors.map(msg1 => Library.cat_message(msg1, msg2)))
     }
 
+    val no_header = Header(Nil, Nil, Nil)
     def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
 
-    val no_header = bad_header("No theory header")
-
     object Name
     {
       val empty = Name("")
@@ -171,12 +170,17 @@
     type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
     type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
 
-    val empty_perspective_text: Perspective_Text =
+    val no_perspective_text: Perspective_Text =
       Perspective(false, Text.Perspective.empty, Overlays.empty)
 
-    val empty_perspective_command: Perspective_Command =
+    val no_perspective_command: Perspective_Command =
       Perspective(false, Command.Perspective.empty, Overlays.empty)
 
+    def is_no_perspective_command(perspective: Perspective_Command): Boolean =
+      !perspective.required &&
+      perspective.visible.is_empty &&
+      perspective.overlays.is_empty
+
 
     /* commands */
 
@@ -237,10 +241,19 @@
 
   final class Node private(
     val get_blob: Option[Document.Blob] = None,
-    val header: Node.Header = Node.bad_header("Bad theory header"),
-    val perspective: Node.Perspective_Command = Node.empty_perspective_command,
+    val header: Node.Header = Node.no_header,
+    val perspective: Node.Perspective_Command = Node.no_perspective_command,
     _commands: Node.Commands = Node.Commands.empty)
   {
+    def is_empty: Boolean =
+      get_blob.isEmpty &&
+      header == Node.no_header &&
+      Node.is_no_perspective_command(perspective) &&
+      commands.isEmpty
+
+    def commands: Linear_Set[Command] = _commands.commands
+    def load_commands: List[Command] = _commands.load_commands
+
     def clear: Node = new Node(header = header)
 
     def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
@@ -256,9 +269,6 @@
       perspective.visible.same(other_perspective.visible) &&
       perspective.overlays == other_perspective.overlays
 
-    def commands: Linear_Set[Command] = _commands.commands
-    def load_commands: List[Command] = _commands.load_commands
-
     def update_commands(new_commands: Linear_Set[Command]): Node =
       if (new_commands eq _commands.commands) this
       else new Node(get_blob, header, perspective, Node.Commands(new_commands))
diff -r 416ce9617780 -r df1b3452d71c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Jul 23 11:53:34 2014 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Jul 23 13:01:30 2014 +0200
@@ -89,19 +89,22 @@
   def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
     : Document.Node.Header =
   {
-    try {
-      val header = Thy_Header.read(reader).decode_symbols
+    if (reader.source.length > 0) {
+      try {
+        val header = Thy_Header.read(reader).decode_symbols
 
-      val base_name = Long_Name.base_name(name.theory)
-      val name1 = header.name
-      if (base_name != name1)
-        error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
-          " for theory " + quote(name1))
+        val base_name = Long_Name.base_name(name.theory)
+        val name1 = header.name
+        if (base_name != name1)
+          error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
+            " for theory " + quote(name1))
 
-      val imports = header.imports.map(import_name(qualifier, name, _))
-      Document.Node.Header(imports, header.keywords, Nil)
+        val imports = header.imports.map(import_name(qualifier, name, _))
+        Document.Node.Header(imports, header.keywords, Nil)
+      }
+      catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     }
-    catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
+    else Document.Node.no_header
   }
 
   def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
diff -r 416ce9617780 -r df1b3452d71c src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 11:53:34 2014 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 13:01:30 2014 +0200
@@ -129,7 +129,7 @@
           Text.Perspective(document_view_ranges ::: load_ranges),
           PIDE.editor.node_overlays(node_name)))
     }
-    else (false, Document.Node.empty_perspective_text)
+    else (false, Document.Node.no_perspective_text)
   }
 
 
@@ -188,7 +188,7 @@
   {
     private var pending_clear = false
     private val pending = new mutable.ListBuffer[Text.Edit]
-    private var last_perspective = Document.Node.empty_perspective_text
+    private var last_perspective = Document.Node.no_perspective_text
 
     def is_pending(): Boolean = pending_clear || !pending.isEmpty
     def snapshot(): List[Text.Edit] = pending.toList
diff -r 416ce9617780 -r df1b3452d71c src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 11:53:34 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 13:01:30 2014 +0200
@@ -38,7 +38,7 @@
     val removed = removed_nodes; removed_nodes = Set.empty
     val removed_perspective =
       (removed -- models.iterator.map(_.node_name)).toList.map(
-        name => (name, Document.Node.empty_perspective_text))
+        name => (name, Document.Node.no_perspective_text))
 
     val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
     if (!edits.isEmpty) session.update(doc_blobs, edits)
diff -r 416ce9617780 -r df1b3452d71c src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 11:53:34 2014 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 13:01:30 2014 +0200
@@ -197,13 +197,14 @@
     val snapshot = PIDE.session.snapshot()
 
     val iterator =
-      (restriction match {
+      restriction match {
         case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
         case None => snapshot.version.nodes.iterator
-      }).filter(_._1.is_theory)
+      }
     val nodes_status1 =
       (nodes_status /: iterator)({ case (status, (name, node)) =>
-          if (PIDE.resources.loaded_theories(name.theory)) status
+          if (!name.is_theory || PIDE.resources.loaded_theories(name.theory)) status
+          else if (node.is_empty) status - name
           else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
     if (nodes_status != nodes_status1) {