tuned;
authorwenzelm
Sat Aug 14 11:52:24 2010 +0200 (2010-08-14 ago)
changeset 38373e8197eea3cd0
parent 38372 e753f71b6b34
child 38374 7eb0f6991e25
tuned;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_node.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Fri Aug 13 21:33:13 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Sat Aug 14 11:52:24 2010 +0200
     1.3 @@ -148,8 +148,7 @@
     1.4  
     1.5  class Command(
     1.6      val id: Document.Command_ID,
     1.7 -    val span: Thy_Syntax.Span,
     1.8 -    val static_parent: Option[Command] = None)  // FIXME !?
     1.9 +    val span: List[Token])
    1.10  {
    1.11    /* classification */
    1.12  
     2.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 13 21:33:13 2010 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 14 11:52:24 2010 +0200
     2.3 @@ -8,9 +8,9 @@
     2.4  signature DOCUMENT =
     2.5  sig
     2.6    type id = int
     2.7 -  type exec_id = id
     2.8 +  type version_id = id
     2.9    type command_id = id
    2.10 -  type version_id = id
    2.11 +  type exec_id = id
    2.12    val no_id: id
    2.13    val parse_id: string -> id
    2.14    val print_id: id -> string
    2.15 @@ -23,9 +23,9 @@
    2.16  (* unique identifiers *)
    2.17  
    2.18  type id = int;
    2.19 -type exec_id = id;
    2.20 +type version_id = id;
    2.21  type command_id = id;
    2.22 -type version_id = id;
    2.23 +type exec_id = id;
    2.24  
    2.25  val no_id = 0;
    2.26  
     3.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 13 21:33:13 2010 +0200
     3.2 +++ b/src/Pure/PIDE/document.scala	Sat Aug 14 11:52:24 2010 +0200
     3.3 @@ -17,9 +17,9 @@
     3.4    /* formal identifiers */
     3.5  
     3.6    type ID = Long
     3.7 -  type Exec_ID = ID
     3.8 +  type Version_ID = ID
     3.9    type Command_ID = ID
    3.10 -  type Version_ID = ID
    3.11 +  type Exec_ID = ID
    3.12  
    3.13    val NO_ID: ID = 0
    3.14  
    3.15 @@ -187,7 +187,7 @@
    3.16      }
    3.17  
    3.18  
    3.19 -    /* phase 3: resulting document edits */
    3.20 +    /* resulting document edits */
    3.21  
    3.22      {
    3.23        val doc_edits = new mutable.ListBuffer[Edit[Command]]
    3.24 @@ -216,10 +216,10 @@
    3.25  
    3.26    /** global state -- accumulated prover results **/
    3.27  
    3.28 -  class Failed_State(state: State) extends Exception
    3.29 -
    3.30    object State
    3.31    {
    3.32 +    class Fail(state: State) extends Exception
    3.33 +
    3.34      val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
    3.35  
    3.36      class Assignment(former_assignment: Map[Command, Exec_ID])
    3.37 @@ -237,20 +237,13 @@
    3.38    }
    3.39  
    3.40    case class State(
    3.41 +    val documents: Map[Version_ID, Document] = Map(),
    3.42      val commands: Map[Command_ID, Command.State] = Map(),
    3.43 -    val documents: Map[Version_ID, Document] = Map(),
    3.44      val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
    3.45      val assignments: Map[Document, State.Assignment] = Map(),
    3.46      val disposed: Set[ID] = Set())  // FIXME unused!?
    3.47    {
    3.48 -    private def fail[A]: A = throw new Failed_State(this)
    3.49 -
    3.50 -    def define_command(command: Command): State =
    3.51 -    {
    3.52 -      val id = command.id
    3.53 -      if (commands.isDefinedAt(id) || disposed(id)) fail
    3.54 -      copy(commands = commands + (id -> command.empty_state))
    3.55 -    }
    3.56 +    private def fail[A]: A = throw new State.Fail(this)
    3.57  
    3.58      def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
    3.59      {
    3.60 @@ -260,9 +253,17 @@
    3.61          assignments = assignments + (document -> new State.Assignment(former_assignment)))
    3.62      }
    3.63  
    3.64 +    def define_command(command: Command): State =
    3.65 +    {
    3.66 +      val id = command.id
    3.67 +      if (commands.isDefinedAt(id) || disposed(id)) fail
    3.68 +      copy(commands = commands + (id -> command.empty_state))
    3.69 +    }
    3.70 +
    3.71      def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
    3.72 +
    3.73 +    def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
    3.74      def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
    3.75 -    def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
    3.76      def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
    3.77      def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
    3.78  
     4.1 --- a/src/Pure/PIDE/markup_node.scala	Fri Aug 13 21:33:13 2010 +0200
     4.2 +++ b/src/Pure/PIDE/markup_node.scala	Sat Aug 14 11:52:24 2010 +0200
     4.3 @@ -2,7 +2,7 @@
     4.4      Author:     Fabian Immler, TU Munich
     4.5      Author:     Makarius
     4.6  
     4.7 -Document markup nodes, with connection to Swing tree model.
     4.8 +Text markup nodes.
     4.9  */
    4.10  
    4.11  package isabelle
    4.12 @@ -78,8 +78,7 @@
    4.13  
    4.14  case class Markup_Text(val markup: List[Markup_Tree], val content: String)
    4.15  {
    4.16 -  private lazy val root =
    4.17 -    new Markup_Tree(new Markup_Node(0, content.length, None), markup)
    4.18 +  private val root = new Markup_Tree(new Markup_Node(0, content.length, None), markup)  // FIXME !?
    4.19  
    4.20    def + (new_tree: Markup_Tree): Markup_Text =
    4.21      new Markup_Text((root + new_tree).branches, content)
     5.1 --- a/src/Pure/System/session.scala	Fri Aug 13 21:33:13 2010 +0200
     5.2 +++ b/src/Pure/System/session.scala	Sat Aug 14 11:52:24 2010 +0200
     5.3 @@ -139,12 +139,12 @@
     5.4              indicate_command_change(st.command)  // FIXME forward Command.State (!?)
     5.5            }
     5.6            catch {
     5.7 -            case _: Document.Failed_State =>
     5.8 +            case _: Document.State.Fail =>
     5.9                if (result.is_status) {
    5.10                  result.body match {
    5.11                    case List(Isar_Document.Assign(edits)) =>
    5.12                      try { change_state(_.assign(target_id, edits)) }
    5.13 -                    catch { case _: Document.Failed_State => bad_result(result) }
    5.14 +                    catch { case _: Document.State.Fail => bad_result(result) }
    5.15                    case _ => bad_result(result)
    5.16                  }
    5.17                }
     6.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 13 21:33:13 2010 +0200
     6.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat Aug 14 11:52:24 2010 +0200
     6.3 @@ -12,11 +12,9 @@
     6.4  
     6.5  object Thy_Syntax
     6.6  {
     6.7 -  type Span = List[Token]
     6.8 -
     6.9 -  def parse_spans(toks: List[Token]): List[Span] =
    6.10 +  def parse_spans(toks: List[Token]): List[List[Token]] =
    6.11    {
    6.12 -    val result = new mutable.ListBuffer[Span]
    6.13 +    val result = new mutable.ListBuffer[List[Token]]
    6.14      val span = new mutable.ListBuffer[Token]
    6.15      val whitespace = new mutable.ListBuffer[Token]
    6.16