--- a/src/Pure/PIDE/command.scala Fri Jul 05 15:38:03 2013 +0200
+++ b/src/Pure/PIDE/command.scala Fri Jul 05 16:01:45 2013 +0200
@@ -75,7 +75,7 @@
private def add_status(st: Markup): State = copy(status = st :: status)
private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
- def + (alt_id: Document_ID.ID, message: XML.Elem): State =
+ def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
--- a/src/Pure/PIDE/document.scala Fri Jul 05 15:38:03 2013 +0200
+++ b/src/Pure/PIDE/document.scala Fri Jul 05 16:01:45 2013 +0200
@@ -334,7 +334,7 @@
def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
- def find_command(version: Version, id: Document_ID.ID): Option[(Node, Command)] =
+ def find_command(version: Version, id: Document_ID.Generic): Option[(Node, Command)] =
commands.get(id) orElse execs.get(id) match {
case None => None
case Some(st) =>
@@ -349,7 +349,7 @@
def the_assignment(version: Version): State.Assignment =
assignments.getOrElse(version.id, fail)
- def accumulate(id: Document_ID.ID, message: XML.Elem): (Command.State, State) =
+ def accumulate(id: Document_ID.Generic, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
case Some(st) =>
val new_st = st + (id, message)
--- a/src/Pure/PIDE/document_id.ML Fri Jul 05 15:38:03 2013 +0200
+++ b/src/Pure/PIDE/document_id.ML Fri Jul 05 16:01:45 2013 +0200
@@ -8,23 +8,23 @@
signature DOCUMENT_ID =
sig
- type id = int
- type version = id
- type command = id
- type exec = id
- val none: id
- val make: unit -> id
- val parse: string -> id
- val print: id -> string
+ type generic = int
+ type version = generic
+ type command = generic
+ type exec = generic
+ val none: generic
+ val make: unit -> generic
+ val parse: string -> generic
+ val print: generic -> string
end;
structure Document_ID: DOCUMENT_ID =
struct
-type id = int;
-type version = id;
-type command = id;
-type exec = id;
+type generic = int;
+type version = generic;
+type command = generic;
+type exec = generic;
val none = 0;
val make = Synchronized.counter ();
--- a/src/Pure/PIDE/document_id.scala Fri Jul 05 15:38:03 2013 +0200
+++ b/src/Pure/PIDE/document_id.scala Fri Jul 05 16:01:45 2013 +0200
@@ -11,14 +11,15 @@
object Document_ID
{
- type ID = Long
- val ID = Properties.Value.Long
+ type Generic = Long
+ type Version = Generic
+ type Command = Generic
+ type Exec = Generic
- type Version = ID
- type Command = ID
- type Exec = ID
+ val none: Generic = 0
+ val make = Counter()
- val none: ID = 0
- val make = Counter()
+ def apply(id: Generic): String = Properties.Value.Long.apply(id)
+ def unapply(s: String): Option[Generic] = Properties.Value.Long.unapply(s)
}
--- a/src/Pure/PIDE/protocol.scala Fri Jul 05 15:38:03 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Jul 05 16:01:45 2013 +0200
@@ -86,7 +86,7 @@
object Command_Timing
{
- def unapply(props: Properties.T): Option[(Document_ID.ID, isabelle.Timing)] =
+ def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
props match {
case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
(args, args) match {
@@ -233,7 +233,7 @@
object Dialog_Args
{
- def unapply(props: Properties.T): Option[(Document_ID.ID, Long, String)] =
+ def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
(props, props, props) match {
case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
Some((id, serial, result))
@@ -243,7 +243,7 @@
object Dialog
{
- def unapply(tree: XML.Tree): Option[(Document_ID.ID, Long, String)] =
+ def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
tree match {
case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
Some((id, serial, result))
@@ -253,7 +253,7 @@
object Dialog_Result
{
- def apply(id: Document_ID.ID, serial: Long, result: String): XML.Elem =
+ def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
{
val props = Position.Id(id) ::: Markup.Serial(serial)
XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
@@ -309,7 +309,7 @@
def define_command(command: Command): Unit =
input("Document.define_command",
- Document_ID.ID(command.id), encode(command.name), encode(command.source))
+ Document_ID(command.id), encode(command.name), encode(command.source))
/* document versions */
@@ -346,7 +346,7 @@
pair(string, encode_edit(name))(name.node, edit)
})
YXML.string_of_body(encode_edits(edits)) }
- input("Document.update", Document_ID.ID(old_id), Document_ID.ID(new_id), edits_yxml)
+ input("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml)
}
def remove_versions(versions: List[Document.Version])
--- a/src/Pure/System/session.scala Fri Jul 05 15:38:03 2013 +0200
+++ b/src/Pure/System/session.scala Fri Jul 05 16:01:45 2013 +0200
@@ -26,7 +26,7 @@
case class Global_Options(options: Options)
case object Caret_Focus
case class Raw_Edits(edits: List[Document.Edit_Text])
- case class Dialog_Result(id: Document_ID.ID, serial: Long, result: String)
+ case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
case class Commands_Changed(
assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
@@ -374,7 +374,7 @@
System.err.println("Ignoring prover output: " + output.message.toString)
}
- def accumulate(state_id: Document_ID.ID, message: XML.Elem)
+ def accumulate(state_id: Document_ID.Generic, message: XML.Elem)
{
try {
val st = global_state >>> (_.accumulate(state_id, message))
@@ -548,6 +548,6 @@
def update_options(options: Options)
{ session_actor !? Update_Options(options) }
- def dialog_result(id: Document_ID.ID, serial: Long, result: String)
+ def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
{ session_actor ! Session.Dialog_Result(id, serial, result) }
}
--- a/src/Tools/jEdit/src/active.scala Fri Jul 05 15:38:03 2013 +0200
+++ b/src/Tools/jEdit/src/active.scala Fri Jul 05 16:01:45 2013 +0200
@@ -26,7 +26,7 @@
val buffer = model.buffer
val snapshot = model.snapshot()
- def try_replace_command(exec_id: Document_ID.ID, s: String)
+ def try_replace_command(exec_id: Document_ID.Exec, s: String)
{
snapshot.state.execs.get(exec_id).map(_.command) match {
case Some(command) =>