src/Pure/PIDE/document.scala
changeset 57615 df1b3452d71c
parent 57614 416ce9617780
child 57616 50ab1db5c0fd
     1.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 23 11:53:34 2014 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed Jul 23 13:01:30 2014 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4      sealed case class Header(
     1.5        imports: List[Name],
     1.6        keywords: Thy_Header.Keywords,
     1.7 -      errors: List[String] = Nil)
     1.8 +      errors: List[String])
     1.9      {
    1.10        def error(msg: String): Header = copy(errors = errors ::: List(msg))
    1.11  
    1.12 @@ -95,10 +95,9 @@
    1.13          copy(errors = errors.map(msg1 => Library.cat_message(msg1, msg2)))
    1.14      }
    1.15  
    1.16 +    val no_header = Header(Nil, Nil, Nil)
    1.17      def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
    1.18  
    1.19 -    val no_header = bad_header("No theory header")
    1.20 -
    1.21      object Name
    1.22      {
    1.23        val empty = Name("")
    1.24 @@ -171,12 +170,17 @@
    1.25      type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
    1.26      type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
    1.27  
    1.28 -    val empty_perspective_text: Perspective_Text =
    1.29 +    val no_perspective_text: Perspective_Text =
    1.30        Perspective(false, Text.Perspective.empty, Overlays.empty)
    1.31  
    1.32 -    val empty_perspective_command: Perspective_Command =
    1.33 +    val no_perspective_command: Perspective_Command =
    1.34        Perspective(false, Command.Perspective.empty, Overlays.empty)
    1.35  
    1.36 +    def is_no_perspective_command(perspective: Perspective_Command): Boolean =
    1.37 +      !perspective.required &&
    1.38 +      perspective.visible.is_empty &&
    1.39 +      perspective.overlays.is_empty
    1.40 +
    1.41  
    1.42      /* commands */
    1.43  
    1.44 @@ -237,10 +241,19 @@
    1.45  
    1.46    final class Node private(
    1.47      val get_blob: Option[Document.Blob] = None,
    1.48 -    val header: Node.Header = Node.bad_header("Bad theory header"),
    1.49 -    val perspective: Node.Perspective_Command = Node.empty_perspective_command,
    1.50 +    val header: Node.Header = Node.no_header,
    1.51 +    val perspective: Node.Perspective_Command = Node.no_perspective_command,
    1.52      _commands: Node.Commands = Node.Commands.empty)
    1.53    {
    1.54 +    def is_empty: Boolean =
    1.55 +      get_blob.isEmpty &&
    1.56 +      header == Node.no_header &&
    1.57 +      Node.is_no_perspective_command(perspective) &&
    1.58 +      commands.isEmpty
    1.59 +
    1.60 +    def commands: Linear_Set[Command] = _commands.commands
    1.61 +    def load_commands: List[Command] = _commands.load_commands
    1.62 +
    1.63      def clear: Node = new Node(header = header)
    1.64  
    1.65      def init_blob(blob: Document.Blob): Node = new Node(Some(blob.unchanged))
    1.66 @@ -256,9 +269,6 @@
    1.67        perspective.visible.same(other_perspective.visible) &&
    1.68        perspective.overlays == other_perspective.overlays
    1.69  
    1.70 -    def commands: Linear_Set[Command] = _commands.commands
    1.71 -    def load_commands: List[Command] = _commands.load_commands
    1.72 -
    1.73      def update_commands(new_commands: Linear_Set[Command]): Node =
    1.74        if (new_commands eq _commands.commands) this
    1.75        else new Node(get_blob, header, perspective, Node.Commands(new_commands))