--- a/src/Pure/PIDE/document.scala Sat May 08 21:08:30 2010 +0200
+++ b/src/Pure/PIDE/document.scala Sat May 08 21:17:42 2010 +0200
@@ -32,13 +32,6 @@
}
- // FIXME
- var phase0: List[Text_Edit] = null
- var phase1: Linear_Set[Command] = null
- var phase2: Linear_Set[Command] = null
- var phase3: List[Edit] = null
-
-
/** document edits **/
@@ -57,8 +50,6 @@
def is_unparsed(command: Command) = command.id == null
- assert(!old_doc.commands.exists(is_unparsed)) // FIXME remove
-
/* phase 1: edit individual command source */
@@ -137,11 +128,6 @@
val former_states = old_doc.assignment.join -- removed_commands
- phase0 = edits
- phase1 = commands1
- phase2 = commands2
- phase3 = doc_edits
-
(doc_edits, new Document(new_id, commands2, former_states))
}
result