slightly more abstract Command.Perspective;
authorwenzelm
Thu Aug 25 11:41:48 2011 +0200 (2011-08-25)
changeset 44474681447a9ffe5
parent 44473 4f264fdf8d0e
child 44475 709e1d671483
slightly more abstract Command.Perspective;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/isar_document.scala
src/Pure/PIDE/text.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Aug 25 11:27:37 2011 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Aug 25 11:41:48 2011 +0200
     1.3 @@ -88,14 +88,22 @@
     1.4  
     1.5    /* perspective */
     1.6  
     1.7 -  type Perspective = List[Command]  // visible commands in canonical order
     1.8 +  object Perspective
     1.9 +  {
    1.10 +    val empty: Perspective = Perspective(Nil)
    1.11 +  }
    1.12  
    1.13 -  def equal_perspective(p1: Perspective, p2: Perspective): Boolean =
    1.14 +  sealed case class Perspective(commands: List[Command])  // visible commands in canonical order
    1.15    {
    1.16 -    require(p1.forall(_.is_defined))
    1.17 -    require(p2.forall(_.is_defined))
    1.18 -    p1.length == p2.length &&
    1.19 -      (p1.iterator zip p2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
    1.20 +    def same(that: Perspective): Boolean =
    1.21 +    {
    1.22 +      val cmds1 = this.commands
    1.23 +      val cmds2 = that.commands
    1.24 +      require(cmds1.forall(_.is_defined))
    1.25 +      require(cmds2.forall(_.is_defined))
    1.26 +      cmds1.length == cmds2.length &&
    1.27 +        (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id })
    1.28 +    }
    1.29    }
    1.30  }
    1.31  
     2.1 --- a/src/Pure/PIDE/document.scala	Thu Aug 25 11:27:37 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Aug 25 11:41:48 2011 +0200
     2.3 @@ -60,7 +60,8 @@
     2.4          case exn => exn
     2.5        }
     2.6  
     2.7 -    val empty: Node = Node(Exn.Exn(ERROR("Bad theory header")), Nil, Map(), Linear_Set())
     2.8 +    val empty: Node =
     2.9 +      Node(Exn.Exn(ERROR("Bad theory header")), Command.Perspective.empty, Map(), Linear_Set())
    2.10  
    2.11      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    2.12        : Iterator[(Command, Text.Offset)] =
     3.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Aug 25 11:27:37 2011 +0200
     3.2 +++ b/src/Pure/PIDE/isar_document.scala	Thu Aug 25 11:41:48 2011 +0200
     3.3 @@ -144,7 +144,7 @@
     3.4    {
     3.5      val ids =
     3.6      { import XML.Encode._
     3.7 -      list(long)(perspective.map(_.id)) }
     3.8 +      list(long)(perspective.commands.map(_.id)) }
     3.9  
    3.10      input("Isar_Document.update_perspective", Document.ID(old_id), Document.ID(new_id), name,
    3.11        YXML.string_of_body(ids))
    3.12 @@ -164,7 +164,7 @@
    3.13              { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
    3.14                  (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) },
    3.15              { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
    3.16 -            { case Document.Node.Perspective(cs) => (cs.map(c => long_atom(c.id)), Nil) }))))
    3.17 +            { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))))
    3.18        YXML.string_of_body(encode(edits)) }
    3.19  
    3.20      input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
     4.1 --- a/src/Pure/PIDE/text.scala	Thu Aug 25 11:27:37 2011 +0200
     4.2 +++ b/src/Pure/PIDE/text.scala	Thu Aug 25 11:41:48 2011 +0200
     4.3 @@ -64,7 +64,7 @@
     4.4  
     4.5    object Perspective
     4.6    {
     4.7 -    val empty = Perspective(Nil)
     4.8 +    val empty: Perspective = Perspective(Nil)
     4.9  
    4.10      def apply(ranges: Seq[Range]): Perspective =
    4.11      {
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 25 11:27:37 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 25 11:41:48 2011 +0200
     5.3 @@ -101,7 +101,7 @@
     5.4  
     5.5    def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
     5.6    {
     5.7 -    if (perspective.is_empty) Nil
     5.8 +    if (perspective.is_empty) Command.Perspective.empty
     5.9      else {
    5.10        val result = new mutable.ListBuffer[Command]
    5.11        @tailrec
    5.12 @@ -121,7 +121,7 @@
    5.13          }
    5.14        }
    5.15        check_ranges(perspective.ranges, node.command_range(perspective.range).toStream)
    5.16 -      result.toList
    5.17 +      Command.Perspective(result.toList)
    5.18      }
    5.19    }
    5.20  
    5.21 @@ -131,7 +131,7 @@
    5.22      val node = nodes(name)
    5.23      val perspective = command_perspective(node, text_perspective)
    5.24      val new_nodes =
    5.25 -      if (Command.equal_perspective(node.perspective, perspective)) None
    5.26 +      if (node.perspective same perspective) None
    5.27        else Some(nodes + (name -> node.copy(perspective = perspective)))
    5.28      (perspective, new_nodes)
    5.29    }