src/Pure/Thy/thy_syntax.scala
changeset 44436 546adfa8a6fc
parent 44388 5f9ad3583e0a
child 44443 35d67b2056cc
     1.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 23 21:19:24 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 24 13:03:39 2011 +0200
     1.3 @@ -97,7 +97,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -  /** command perspective **/
     1.8 +  /** perspective **/
     1.9  
    1.10    def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
    1.11    {
    1.12 @@ -126,6 +126,26 @@
    1.13      }
    1.14    }
    1.15  
    1.16 +  def update_perspective(nodes: Document.Nodes, name: String, text_perspective: Text.Perspective)
    1.17 +    : (Command.Perspective, Option[Document.Nodes]) =
    1.18 +  {
    1.19 +    val node = nodes(name)
    1.20 +    val perspective = command_perspective(node, text_perspective)
    1.21 +    val new_nodes =
    1.22 +      if (Command.equal_perspective(node.perspective, perspective)) None
    1.23 +      else Some(nodes + (name -> node.copy(perspective = perspective)))
    1.24 +    (perspective, new_nodes)
    1.25 +  }
    1.26 +
    1.27 +  def edit_perspective(previous: Document.Version, name: String, text_perspective: Text.Perspective)
    1.28 +    : (Command.Perspective, Document.Version) =
    1.29 +  {
    1.30 +    val nodes = previous.nodes
    1.31 +    val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
    1.32 +    val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
    1.33 +    (perspective, version)
    1.34 +  }
    1.35 +
    1.36  
    1.37  
    1.38    /** text edits **/
    1.39 @@ -243,11 +263,11 @@
    1.40            }
    1.41  
    1.42          case (name, Document.Node.Perspective(text_perspective)) =>
    1.43 -          val node = nodes(name)
    1.44 -          val perspective = command_perspective(node, text_perspective)
    1.45 -          if (!Command.equal_perspective(node.perspective, perspective)) {
    1.46 -            doc_edits += (name -> Document.Node.Perspective(perspective))
    1.47 -            nodes += (name -> node.copy(perspective = perspective))
    1.48 +          update_perspective(nodes, name, text_perspective) match {
    1.49 +            case (_, None) =>
    1.50 +            case (perspective, Some(nodes1)) =>
    1.51 +              doc_edits += (name -> Document.Node.Perspective(perspective))
    1.52 +              nodes = nodes1
    1.53            }
    1.54        }
    1.55        (doc_edits.toList, Document.Version(Document.new_id(), nodes))