more explicit discrimination of empty nodes -- suppress from Theories panel;
authorwenzelm
Wed Jul 23 13:01:30 2014 +0200 (2014-07-23)
changeset 57615df1b3452d71c
parent 57614 416ce9617780
child 57616 50ab1db5c0fd
more explicit discrimination of empty nodes -- suppress from Theories panel;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Jul 23 11:53:34 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Jul 23 13:01:30 2014 +0200
     1.3 @@ -314,6 +314,8 @@
     1.4  
     1.5    sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
     1.6    {
     1.7 +    def is_empty: Boolean = commands.isEmpty
     1.8 +
     1.9      def same(that: Perspective): Boolean =
    1.10      {
    1.11        val cmds1 = this.commands
     2.1 --- a/src/Pure/PIDE/document.ML	Wed Jul 23 11:53:34 2014 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Wed Jul 23 13:01:30 2014 +0200
     2.3 @@ -72,11 +72,23 @@
     2.4    visible_last = try List.last command_ids,
     2.5    overlays = Inttab.make_list overlays};
     2.6  
     2.7 -val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["No theory header"]);
     2.8 +val no_header = ("", Thy_Header.make ("", Position.none) [] [], []);
     2.9  val no_perspective = make_perspective (false, [], []);
    2.10  
    2.11  val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
    2.12  
    2.13 +fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
    2.14 +  not required andalso
    2.15 +  Inttab.is_empty visible andalso
    2.16 +  is_none visible_last andalso
    2.17 +  Inttab.is_empty overlays;
    2.18 +
    2.19 +fun is_empty_node (Node {header, perspective, entries, result}) =
    2.20 +  header = no_header andalso
    2.21 +  is_no_perspective perspective andalso
    2.22 +  Entries.is_empty entries andalso
    2.23 +  is_none result;
    2.24 +
    2.25  
    2.26  (* basic components *)
    2.27  
     3.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 23 11:53:34 2014 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 23 13:01:30 2014 +0200
     3.3 @@ -87,7 +87,7 @@
     3.4      sealed case class Header(
     3.5        imports: List[Name],
     3.6        keywords: Thy_Header.Keywords,
     3.7 -      errors: List[String] = Nil)
     3.8 +      errors: List[String])
     3.9      {
    3.10        def error(msg: String): Header = copy(errors = errors ::: List(msg))
    3.11  
    3.12 @@ -95,10 +95,9 @@
    3.13          copy(errors = errors.map(msg1 => Library.cat_message(msg1, msg2)))
    3.14      }
    3.15  
    3.16 +    val no_header = Header(Nil, Nil, Nil)
    3.17      def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
    3.18  
    3.19 -    val no_header = bad_header("No theory header")
    3.20 -
    3.21      object Name
    3.22      {
    3.23        val empty = Name("")
    3.24 @@ -171,12 +170,17 @@
    3.25      type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
    3.26      type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
    3.27  
    3.28 -    val empty_perspective_text: Perspective_Text =
    3.29 +    val no_perspective_text: Perspective_Text =
    3.30        Perspective(false, Text.Perspective.empty, Overlays.empty)
    3.31  
    3.32 -    val empty_perspective_command: Perspective_Command =
    3.33 +    val no_perspective_command: Perspective_Command =
    3.34        Perspective(false, Command.Perspective.empty, Overlays.empty)
    3.35  
    3.36 +    def is_no_perspective_command(perspective: Perspective_Command): Boolean =
    3.37 +      !perspective.required &&
    3.38 +      perspective.visible.is_empty &&
    3.39 +      perspective.overlays.is_empty
    3.40 +
    3.41  
    3.42      /* commands */
    3.43  
    3.44 @@ -237,10 +241,19 @@
    3.45  
    3.46    final class Node private(
    3.47      val get_blob: Option[Document.Blob] = None,
    3.48 -    val header: Node.Header = Node.bad_header("Bad theory header"),
    3.49 -    val perspective: Node.Perspective_Command = Node.empty_perspective_command,
    3.50 +    val header: Node.Header = Node.no_header,
    3.51 +    val perspective: Node.Perspective_Command = Node.no_perspective_command,
    3.52      _commands: Node.Commands = Node.Commands.empty)
    3.53    {
    3.54 +    def is_empty: Boolean =
    3.55 +      get_blob.isEmpty &&
    3.56 +      header == Node.no_header &&
    3.57 +      Node.is_no_perspective_command(perspective) &&
    3.58 +      commands.isEmpty
    3.59 +
    3.60 +    def commands: Linear_Set[Command] = _commands.commands
    3.61 +    def load_commands: List[Command] = _commands.load_commands
    3.62 +
    3.63      def clear: Node = new Node(header = header)
    3.64  
    3.65      def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
    3.66 @@ -256,9 +269,6 @@
    3.67        perspective.visible.same(other_perspective.visible) &&
    3.68        perspective.overlays == other_perspective.overlays
    3.69  
    3.70 -    def commands: Linear_Set[Command] = _commands.commands
    3.71 -    def load_commands: List[Command] = _commands.load_commands
    3.72 -
    3.73      def update_commands(new_commands: Linear_Set[Command]): Node =
    3.74        if (new_commands eq _commands.commands) this
    3.75        else new Node(get_blob, header, perspective, Node.Commands(new_commands))
     4.1 --- a/src/Pure/PIDE/resources.scala	Wed Jul 23 11:53:34 2014 +0200
     4.2 +++ b/src/Pure/PIDE/resources.scala	Wed Jul 23 13:01:30 2014 +0200
     4.3 @@ -89,19 +89,22 @@
     4.4    def check_thy_reader(qualifier: String, name: Document.Node.Name, reader: Reader[Char])
     4.5      : Document.Node.Header =
     4.6    {
     4.7 -    try {
     4.8 -      val header = Thy_Header.read(reader).decode_symbols
     4.9 +    if (reader.source.length > 0) {
    4.10 +      try {
    4.11 +        val header = Thy_Header.read(reader).decode_symbols
    4.12  
    4.13 -      val base_name = Long_Name.base_name(name.theory)
    4.14 -      val name1 = header.name
    4.15 -      if (base_name != name1)
    4.16 -        error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
    4.17 -          " for theory " + quote(name1))
    4.18 +        val base_name = Long_Name.base_name(name.theory)
    4.19 +        val name1 = header.name
    4.20 +        if (base_name != name1)
    4.21 +          error("Bad file name " + Resources.thy_path(Path.basic(base_name)) +
    4.22 +            " for theory " + quote(name1))
    4.23  
    4.24 -      val imports = header.imports.map(import_name(qualifier, name, _))
    4.25 -      Document.Node.Header(imports, header.keywords, Nil)
    4.26 +        val imports = header.imports.map(import_name(qualifier, name, _))
    4.27 +        Document.Node.Header(imports, header.keywords, Nil)
    4.28 +      }
    4.29 +      catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    4.30      }
    4.31 -    catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    4.32 +    else Document.Node.no_header
    4.33    }
    4.34  
    4.35    def check_thy(qualifier: String, name: Document.Node.Name): Document.Node.Header =
     5.1 --- a/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 11:53:34 2014 +0200
     5.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Jul 23 13:01:30 2014 +0200
     5.3 @@ -129,7 +129,7 @@
     5.4            Text.Perspective(document_view_ranges ::: load_ranges),
     5.5            PIDE.editor.node_overlays(node_name)))
     5.6      }
     5.7 -    else (false, Document.Node.empty_perspective_text)
     5.8 +    else (false, Document.Node.no_perspective_text)
     5.9    }
    5.10  
    5.11  
    5.12 @@ -188,7 +188,7 @@
    5.13    {
    5.14      private var pending_clear = false
    5.15      private val pending = new mutable.ListBuffer[Text.Edit]
    5.16 -    private var last_perspective = Document.Node.empty_perspective_text
    5.17 +    private var last_perspective = Document.Node.no_perspective_text
    5.18  
    5.19      def is_pending(): Boolean = pending_clear || !pending.isEmpty
    5.20      def snapshot(): List[Text.Edit] = pending.toList
     6.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 11:53:34 2014 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Wed Jul 23 13:01:30 2014 +0200
     6.3 @@ -38,7 +38,7 @@
     6.4      val removed = removed_nodes; removed_nodes = Set.empty
     6.5      val removed_perspective =
     6.6        (removed -- models.iterator.map(_.node_name)).toList.map(
     6.7 -        name => (name, Document.Node.empty_perspective_text))
     6.8 +        name => (name, Document.Node.no_perspective_text))
     6.9  
    6.10      val edits = models.flatMap(_.flushed_edits(doc_blobs)) ::: removed_perspective
    6.11      if (!edits.isEmpty) session.update(doc_blobs, edits)
     7.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 11:53:34 2014 +0200
     7.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Wed Jul 23 13:01:30 2014 +0200
     7.3 @@ -197,13 +197,14 @@
     7.4      val snapshot = PIDE.session.snapshot()
     7.5  
     7.6      val iterator =
     7.7 -      (restriction match {
     7.8 +      restriction match {
     7.9          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
    7.10          case None => snapshot.version.nodes.iterator
    7.11 -      }).filter(_._1.is_theory)
    7.12 +      }
    7.13      val nodes_status1 =
    7.14        (nodes_status /: iterator)({ case (status, (name, node)) =>
    7.15 -          if (PIDE.resources.loaded_theories(name.theory)) status
    7.16 +          if (!name.is_theory || PIDE.resources.loaded_theories(name.theory)) status
    7.17 +          else if (node.is_empty) status - name
    7.18            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
    7.19  
    7.20      if (nodes_status != nodes_status1) {