--- a/src/Pure/PIDE/command.scala Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/PIDE/command.scala Sat Aug 14 11:52:24 2010 +0200
@@ -148,8 +148,7 @@
class Command(
val id: Document.Command_ID,
- val span: Thy_Syntax.Span,
- val static_parent: Option[Command] = None) // FIXME !?
+ val span: List[Token])
{
/* classification */
--- a/src/Pure/PIDE/document.ML Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/PIDE/document.ML Sat Aug 14 11:52:24 2010 +0200
@@ -8,9 +8,9 @@
signature DOCUMENT =
sig
type id = int
- type exec_id = id
+ type version_id = id
type command_id = id
- type version_id = id
+ type exec_id = id
val no_id: id
val parse_id: string -> id
val print_id: id -> string
@@ -23,9 +23,9 @@
(* unique identifiers *)
type id = int;
-type exec_id = id;
+type version_id = id;
type command_id = id;
-type version_id = id;
+type exec_id = id;
val no_id = 0;
--- a/src/Pure/PIDE/document.scala Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/PIDE/document.scala Sat Aug 14 11:52:24 2010 +0200
@@ -17,9 +17,9 @@
/* formal identifiers */
type ID = Long
- type Exec_ID = ID
+ type Version_ID = ID
type Command_ID = ID
- type Version_ID = ID
+ type Exec_ID = ID
val NO_ID: ID = 0
@@ -187,7 +187,7 @@
}
- /* phase 3: resulting document edits */
+ /* resulting document edits */
{
val doc_edits = new mutable.ListBuffer[Edit[Command]]
@@ -216,10 +216,10 @@
/** global state -- accumulated prover results **/
- class Failed_State(state: State) extends Exception
-
object State
{
+ class Fail(state: State) extends Exception
+
val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
class Assignment(former_assignment: Map[Command, Exec_ID])
@@ -237,20 +237,13 @@
}
case class State(
+ val documents: Map[Version_ID, Document] = Map(),
val commands: Map[Command_ID, Command.State] = Map(),
- val documents: Map[Version_ID, Document] = Map(),
val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
val assignments: Map[Document, State.Assignment] = Map(),
val disposed: Set[ID] = Set()) // FIXME unused!?
{
- private def fail[A]: A = throw new Failed_State(this)
-
- def define_command(command: Command): State =
- {
- val id = command.id
- if (commands.isDefinedAt(id) || disposed(id)) fail
- copy(commands = commands + (id -> command.empty_state))
- }
+ private def fail[A]: A = throw new State.Fail(this)
def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
{
@@ -260,9 +253,17 @@
assignments = assignments + (document -> new State.Assignment(former_assignment)))
}
+ def define_command(command: Command): State =
+ {
+ val id = command.id
+ if (commands.isDefinedAt(id) || disposed(id)) fail
+ copy(commands = commands + (id -> command.empty_state))
+ }
+
def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
+
+ def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
- def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
--- a/src/Pure/PIDE/markup_node.scala Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/PIDE/markup_node.scala Sat Aug 14 11:52:24 2010 +0200
@@ -2,7 +2,7 @@
Author: Fabian Immler, TU Munich
Author: Makarius
-Document markup nodes, with connection to Swing tree model.
+Text markup nodes.
*/
package isabelle
@@ -78,8 +78,7 @@
case class Markup_Text(val markup: List[Markup_Tree], val content: String)
{
- private lazy val root =
- new Markup_Tree(new Markup_Node(0, content.length, None), markup)
+ private val root = new Markup_Tree(new Markup_Node(0, content.length, None), markup) // FIXME !?
def + (new_tree: Markup_Tree): Markup_Text =
new Markup_Text((root + new_tree).branches, content)
--- a/src/Pure/System/session.scala Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/System/session.scala Sat Aug 14 11:52:24 2010 +0200
@@ -139,12 +139,12 @@
indicate_command_change(st.command) // FIXME forward Command.State (!?)
}
catch {
- case _: Document.Failed_State =>
+ case _: Document.State.Fail =>
if (result.is_status) {
result.body match {
case List(Isar_Document.Assign(edits)) =>
try { change_state(_.assign(target_id, edits)) }
- catch { case _: Document.Failed_State => bad_result(result) }
+ catch { case _: Document.State.Fail => bad_result(result) }
case _ => bad_result(result)
}
}
--- a/src/Pure/Thy/thy_syntax.scala Fri Aug 13 21:33:13 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Sat Aug 14 11:52:24 2010 +0200
@@ -12,11 +12,9 @@
object Thy_Syntax
{
- type Span = List[Token]
-
- def parse_spans(toks: List[Token]): List[Span] =
+ def parse_spans(toks: List[Token]): List[List[Token]] =
{
- val result = new mutable.ListBuffer[Span]
+ val result = new mutable.ListBuffer[List[Token]]
val span = new mutable.ListBuffer[Token]
val whitespace = new mutable.ListBuffer[Token]