# HG changeset patch
# User wenzelm
# Date 1273346262 -7200
# Node ID c8ae87ce6e4d4d6015d7a2bbf0c71e32bafa3cd0
# Parent  b82a698ef6c9e19d8a41c9a315de14c837baad3e
removed junk;

diff -r b82a698ef6c9 -r c8ae87ce6e4d src/Pure/PIDE/document.scala
--- 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