--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala Tue Dec 29 15:33:39 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala Tue Dec 29 20:40:08 2009 +0100
@@ -30,7 +30,7 @@
"`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
"[()\\[\\]{}:;]", Pattern.MULTILINE)
- def empty(id: String): Proof_Document =
+ def empty(id: Isar_Document.Document_ID): Proof_Document =
new Proof_Document(id, Linear_Set(), Map(), Linear_Set(), Map())
type StructureChange = List[(Option[Command], Option[Command])]
@@ -38,11 +38,11 @@
class Proof_Document(
- val id: String,
+ val id: Isar_Document.Document_ID,
val tokens: Linear_Set[Token], // FIXME plain List, inside Command
val token_start: Map[Token, Int], // FIXME eliminate
val commands: Linear_Set[Command],
- var states: Map[Command, Command_State]) // FIXME immutable
+ var states: Map[Command, Command_State]) // FIXME immutable, eliminate!?
{
import Proof_Document.StructureChange