1.1 --- a/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 08 14:49:01 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Tue Dec 08 16:30:20 2009 +0100
     1.3 @@ -8,14 +8,13 @@
     1.4  
     1.5  package isabelle.proofdocument
     1.6  
     1.7 +
     1.8  import scala.actors.Actor, Actor._
     1.9  
    1.10  import java.util.regex.Pattern
    1.11  
    1.12 -import isabelle.prover.{Prover, Command, Command_State}
    1.13  
    1.14 -
    1.15 -object ProofDocument
    1.16 +object Proof_Document
    1.17  {
    1.18    // Be careful when changing this regex. Not only must it handle the
    1.19    // spurious end of a token but also:  
    1.20 @@ -34,14 +33,14 @@
    1.21        "[()\\[\\]{}:;]", Pattern.MULTILINE)
    1.22  
    1.23    val empty =
    1.24 -    new ProofDocument(isabelle.jedit.Isabelle.system.id(),
    1.25 +    new Proof_Document(isabelle.jedit.Isabelle.system.id(),
    1.26        Linear_Set(), Map(), Linear_Set(), Map(), _ => false)
    1.27  
    1.28    type StructureChange = List[(Option[Command], Option[Command])]
    1.29  
    1.30  }
    1.31  
    1.32 -class ProofDocument(
    1.33 +class Proof_Document(
    1.34    val id: String,
    1.35    val tokens: Linear_Set[Token],
    1.36    val token_start: Map[Token, Int],
    1.37 @@ -49,10 +48,10 @@
    1.38    var states: Map[Command, Command_State],   // FIXME immutable
    1.39    is_command_keyword: String => Boolean)
    1.40  {
    1.41 -  import ProofDocument.StructureChange
    1.42 +  import Proof_Document.StructureChange
    1.43  
    1.44 -  def set_command_keyword(f: String => Boolean): ProofDocument =
    1.45 -    new ProofDocument(id, tokens, token_start, commands, states, f)
    1.46 +  def set_command_keyword(f: String => Boolean): Proof_Document =
    1.47 +    new Proof_Document(id, tokens, token_start, commands, states, f)
    1.48  
    1.49    def content = Token.string_from_tokens(Nil ++ tokens, token_start)
    1.50  
    1.51 @@ -60,9 +59,9 @@
    1.52    
    1.53    /** token view **/
    1.54  
    1.55 -  def text_changed(change: Change): (ProofDocument, StructureChange) =
    1.56 +  def text_changed(change: Change): (Proof_Document, StructureChange) =
    1.57    {
    1.58 -    def edit_doc(doc_chgs: (ProofDocument, StructureChange), edit: Edit) = {
    1.59 +    def edit_doc(doc_chgs: (Proof_Document, StructureChange), edit: Edit) = {
    1.60        val (doc, chgs) = doc_chgs
    1.61        val (new_doc, chg) = doc.text_edit(edit, change.id)
    1.62        (new_doc, chgs ++ chg)
    1.63 @@ -70,7 +69,7 @@
    1.64      ((this, Nil: StructureChange) /: change.edits)(edit_doc)
    1.65    }
    1.66  
    1.67 -  def text_edit(e: Edit, id: String): (ProofDocument, StructureChange) =
    1.68 +  def text_edit(e: Edit, id: String): (Proof_Document, StructureChange) =
    1.69    {
    1.70      case class TextChange(start: Int, added: String, removed: String)
    1.71      val change = e match {
    1.72 @@ -116,7 +115,7 @@
    1.73  
    1.74      val match_start = invalid_tokens.firstOption.map(start(_)).getOrElse(0)
    1.75      val matcher =
    1.76 -      ProofDocument.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
    1.77 +      Proof_Document.token_pattern.matcher(Token.string_from_tokens(invalid_tokens, start))
    1.78  
    1.79      while (matcher.find() && invalid_tokens != Nil) {
    1.80  			val kind =
    1.81 @@ -158,7 +157,7 @@
    1.82      after_change: Option[Token],
    1.83      new_tokens: List[Token],
    1.84      new_token_start: Map[Token, Int]):
    1.85 -  (ProofDocument, StructureChange) =
    1.86 +  (Proof_Document, StructureChange) =
    1.87    {
    1.88      val new_tokenset = Linear_Set[Token]() ++ new_tokens
    1.89      val cmd_before_change = before_change match {
    1.90 @@ -236,7 +235,7 @@
    1.91  
    1.92  
    1.93      val doc =
    1.94 -      new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,
    1.95 +      new Proof_Document(new_id, new_tokenset, new_token_start, new_commandset,
    1.96          states -- removed_commands, is_command_keyword)
    1.97  
    1.98      val removes =