Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Thy/thy_syntax.scala
changeset 46680 234f1730582d
parent 45644 8634b4e61b88
child 46681 c083a3f621c0 
--- a/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 16:58:28 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 17:15:33 2012 +0100
@@ -135,7 +135,7 @@
     val perspective = command_perspective(node, text_perspective)
     val new_nodes =
       if (node.perspective same perspective) None
-      else Some(nodes + (name -> node.copy(perspective = perspective)))
+      else Some(nodes + (name -> node.update_perspective(perspective)))
     (perspective, new_nodes)
   }
 
@@ -252,7 +252,7 @@
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
           doc_edits += (name -> Document.Node.Edits(cmd_edits))
-          nodes += (name -> node.copy(commands = commands2))
+          nodes += (name -> node.update_commands(commands2))
 
         case (name, Document.Node.Header(header)) =>
           val node = nodes(name)
@@ -263,7 +263,7 @@
             }
           if (update_header) {
             doc_edits += (name -> Document.Node.Header(header))
-            nodes += (name -> node.copy(header = header))
+            nodes += (name -> node.update_header(header))
           }
 
         case (name, Document.Node.Perspective(text_perspective)) =>
isabelle