# HG changeset patch
# User wenzelm
# Date 1373032905 -7200
# Node ID 21f8e0e151f5ce47340ea5e6afaeca12673c60aa
# Parent  99dd8b4ef3fe241fc64338cc50bd297d4078cbb5
tuned signature;

diff -r 99dd8b4ef3fe -r 21f8e0e151f5 src/Pure/PIDE/command.scala
--- 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) =>
diff -r 99dd8b4ef3fe -r 21f8e0e151f5 src/Pure/PIDE/document.scala
--- 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)
diff -r 99dd8b4ef3fe -r 21f8e0e151f5 src/Pure/PIDE/document_id.ML
--- 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 ();
diff -r 99dd8b4ef3fe -r 21f8e0e151f5 src/Pure/PIDE/document_id.scala
--- 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)
 }
 
diff -r 99dd8b4ef3fe -r 21f8e0e151f5 src/Pure/PIDE/protocol.scala
--- 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])
diff -r 99dd8b4ef3fe -r 21f8e0e151f5 src/Pure/System/session.scala
--- 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) }
 }
diff -r 99dd8b4ef3fe -r 21f8e0e151f5 src/Tools/jEdit/src/active.scala
--- 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) =>