1.1 --- a/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 14:09:06 2013 +0200
     1.2 +++ b/src/Pure/Concurrent/synchronized.ML	Fri Jul 05 15:38:03 2013 +0200
     1.3 @@ -69,6 +69,7 @@
     1.4  
     1.5  (* unique identifiers > 0 *)
     1.6  
     1.7 +(*NB: ML ticks forwards, JVM ticks backwards*)
     1.8  fun counter () =
     1.9    let
    1.10      val counter = var "counter" (0: int);

     2.1 --- a/src/Pure/PIDE/command.ML	Fri Jul 05 14:09:06 2013 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Fri Jul 05 15:38:03 2013 +0200
     2.3 @@ -23,8 +23,8 @@
     2.4    val no_eval: eval
     2.5    val eval: span -> Toplevel.transition -> eval_state -> eval_state
     2.6    type print_fn = Toplevel.transition -> Toplevel.state -> unit
     2.7 -  type print = {name: string, pri: int, exec_id: int, print: unit memo}
     2.8 -  val print: (unit -> int) -> string -> eval -> print list
     2.9 +  type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
    2.10 +  val print: string -> eval -> print list
    2.11    val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    2.12  end;
    2.13  
    2.14 @@ -175,7 +175,7 @@
    2.15  
    2.16  (* print *)
    2.17  
    2.18 -type print = {name: string, pri: int, exec_id: int, print: unit memo};
    2.19 +type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo};
    2.20  type print_fn = Toplevel.transition -> Toplevel.state -> unit;
    2.21  
    2.22  local
    2.23 @@ -192,13 +192,13 @@
    2.24  
    2.25  in
    2.26  
    2.27 -fun print new_id command_name eval =
    2.28 +fun print command_name eval =
    2.29    rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
    2.30      (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
    2.31        Exn.Res NONE => NONE
    2.32      | Exn.Res (SOME print_fn) =>
    2.33          let
    2.34 -          val exec_id = new_id ();
    2.35 +          val exec_id = Document_ID.make ();
    2.36            fun body () =
    2.37              let
    2.38                val {failed, command, state = st', ...} = memo_result eval;
    2.39 @@ -207,7 +207,7 @@
    2.40          in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
    2.41      | Exn.Exn exn =>
    2.42          let
    2.43 -          val exec_id = new_id ();
    2.44 +          val exec_id = Document_ID.make ();
    2.45            fun body () =
    2.46              let
    2.47                val {command, ...} = memo_result eval;

     3.1 --- a/src/Pure/PIDE/command.scala	Fri Jul 05 14:09:06 2013 +0200
     3.2 +++ b/src/Pure/PIDE/command.scala	Fri Jul 05 15:38:03 2013 +0200
     3.3 @@ -75,7 +75,7 @@
     3.4      private def add_status(st: Markup): State = copy(status = st :: status)
     3.5      private def add_markup(m: Text.Markup): State = copy(markup = markup + m)
     3.6  
     3.7 -    def + (alt_id: Document.ID, message: XML.Elem): State =
     3.8 +    def + (alt_id: Document_ID.ID, message: XML.Elem): State =
     3.9        message match {
    3.10          case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
    3.11            (this /: msgs)((state, msg) =>
    3.12 @@ -136,7 +136,7 @@
    3.13    type Span = List[Token]
    3.14  
    3.15    def apply(
    3.16 -    id: Document.Command_ID,
    3.17 +    id: Document_ID.Command,
    3.18      node_name: Document.Node.Name,
    3.19      span: Span,
    3.20      results: Results = Results.empty,
    3.21 @@ -160,16 +160,16 @@
    3.22      new Command(id, node_name, span1.toList, source, results, markup)
    3.23    }
    3.24  
    3.25 -  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
    3.26 +  val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil)
    3.27  
    3.28 -  def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree)
    3.29 +  def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
    3.30        : Command =
    3.31      Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
    3.32  
    3.33    def unparsed(source: String): Command =
    3.34 -    unparsed(Document.no_id, source, Results.empty, Markup_Tree.empty)
    3.35 +    unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
    3.36  
    3.37 -  def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
    3.38 +  def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
    3.39    {
    3.40      val text = XML.content(body)
    3.41      val markup = Markup_Tree.from_XML(body)
    3.42 @@ -200,7 +200,7 @@
    3.43  
    3.44  
    3.45  final class Command private(
    3.46 -    val id: Document.Command_ID,
    3.47 +    val id: Document_ID.Command,
    3.48      val node_name: Document.Node.Name,
    3.49      val span: Command.Span,
    3.50      val source: String,
    3.51 @@ -209,7 +209,7 @@
    3.52  {
    3.53    /* classification */
    3.54  
    3.55 -  def is_undefined: Boolean = id == Document.no_id
    3.56 +  def is_undefined: Boolean = id == Document_ID.none
    3.57    val is_unparsed: Boolean = span.exists(_.is_unparsed)
    3.58    val is_unfinished: Boolean = span.exists(_.is_unfinished)
    3.59  

     4.1 --- a/src/Pure/PIDE/document.ML	Fri Jul 05 14:09:06 2013 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Fri Jul 05 15:38:03 2013 +0200
     4.3 @@ -7,31 +7,23 @@
     4.4  
     4.5  signature DOCUMENT =
     4.6  sig
     4.7 -  type id = int
     4.8 -  type version_id = id
     4.9 -  type command_id = id
    4.10 -  type exec_id = id
    4.11 -  val no_id: id
    4.12 -  val new_id: unit -> id
    4.13 -  val parse_id: string -> id
    4.14 -  val print_id: id -> string
    4.15    type node_header = string * Thy_Header.header * string list
    4.16    datatype node_edit =
    4.17      Clear |    (* FIXME unused !? *)
    4.18 -    Edits of (command_id option * command_id option) list |
    4.19 +    Edits of (Document_ID.command option * Document_ID.command option) list |
    4.20      Deps of node_header |
    4.21 -    Perspective of command_id list
    4.22 +    Perspective of Document_ID.command list
    4.23    type edit = string * node_edit
    4.24    type state
    4.25    val init_state: state
    4.26 -  val define_command: command_id -> string -> string -> state -> state
    4.27 -  val remove_versions: version_id list -> state -> state
    4.28 +  val define_command: Document_ID.command -> string -> string -> state -> state
    4.29 +  val remove_versions: Document_ID.version list -> state -> state
    4.30    val discontinue_execution: state -> unit
    4.31    val cancel_execution: state -> unit
    4.32    val start_execution: state -> unit
    4.33    val timing: bool Unsynchronized.ref
    4.34 -  val update: version_id -> version_id -> edit list -> state ->
    4.35 -    (command_id * exec_id list) list * state
    4.36 +  val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    4.37 +    (Document_ID.command * Document_ID.exec list) list * state
    4.38    val state: unit -> state
    4.39    val change_state: (state -> state) -> unit
    4.40  end;
    4.41 @@ -39,27 +31,10 @@
    4.42  structure Document: DOCUMENT =
    4.43  struct
    4.44  
    4.45 -(* unique identifiers *)
    4.46 -
    4.47 -type id = int;
    4.48 -type version_id = id;
    4.49 -type command_id = id;
    4.50 -type exec_id = id;
    4.51 -
    4.52 -val no_id = 0;
    4.53 -val new_id = Synchronized.counter ();
    4.54 -
    4.55 -val parse_id = Markup.parse_int;
    4.56 -val print_id = Markup.print_int;
    4.57 -
    4.58 -fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id);
    4.59 -fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
    4.60 -
    4.61 -
    4.62  (* command execution *)
    4.63  
    4.64 -type exec = exec_id * (Command.eval * Command.print list);  (*eval/print process*)
    4.65 -val no_exec: exec = (no_id, (Command.no_eval, []));
    4.66 +type exec = Document_ID.exec * (Command.eval * Command.print list);  (*eval/print process*)
    4.67 +val no_exec: exec = (Document_ID.none, (Command.no_eval, []));
    4.68  
    4.69  fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
    4.70  
    4.71 @@ -74,9 +49,12 @@
    4.72  
    4.73  (** document structure **)
    4.74  
    4.75 +fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
    4.76 +fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
    4.77 +
    4.78  type node_header = string * Thy_Header.header * string list;
    4.79 -type perspective = Inttab.set * command_id option;
    4.80 -structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    4.81 +type perspective = Inttab.set * Document_ID.command option;
    4.82 +structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
    4.83  
    4.84  abstype node = Node of
    4.85   {header: node_header,  (*master directory, theory header, errors*)
    4.86 @@ -156,9 +134,9 @@
    4.87  
    4.88  datatype node_edit =
    4.89    Clear |
    4.90 -  Edits of (command_id option * command_id option) list |
    4.91 +  Edits of (Document_ID.command option * Document_ID.command option) list |
    4.92    Deps of node_header |
    4.93 -  Perspective of command_id list;
    4.94 +  Perspective of Document_ID.command list;
    4.95  
    4.96  type edit = string * node_edit;
    4.97  
    4.98 @@ -175,7 +153,7 @@
    4.99    | SOME (exec, _) => exec);
   4.100  
   4.101  fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
   4.102 -  | the_default_entry _ NONE = (no_id, no_exec);
   4.103 +  | the_default_entry _ NONE = (Document_ID.none, no_exec);
   4.104  
   4.105  fun update_entry id exec =
   4.106    map_entries (Entries.update (id, exec));
   4.107 @@ -237,7 +215,8 @@
   4.108  abstype state = State of
   4.109   {versions: version Inttab.table,  (*version_id -> document content*)
   4.110    commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
   4.111 -  execution: version_id * Future.group * bool Unsynchronized.ref}  (*current execution process*)
   4.112 +  execution:
   4.113 +    Document_ID.version * Future.group * bool Unsynchronized.ref}  (*current execution process*)
   4.114  with
   4.115  
   4.116  fun make_state (versions, commands, execution) =
   4.117 @@ -247,15 +226,15 @@
   4.118    make_state (f (versions, commands, execution));
   4.119  
   4.120  val init_state =
   4.121 -  make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
   4.122 -    (no_id, Future.new_group NONE, Unsynchronized.ref false));
   4.123 +  make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty,
   4.124 +    (Document_ID.none, Future.new_group NONE, Unsynchronized.ref false));
   4.125  
   4.126  fun execution_of (State {execution, ...}) = execution;
   4.127  
   4.128  
   4.129  (* document versions *)
   4.130  
   4.131 -fun define_version (id: version_id) version =
   4.132 +fun define_version (id: Document_ID.version) version =
   4.133    map_state (fn (versions, commands, _) =>
   4.134      let
   4.135        val versions' = Inttab.update_new (id, version) versions
   4.136 @@ -263,21 +242,21 @@
   4.137        val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
   4.138      in (versions', commands, execution') end);
   4.139  
   4.140 -fun the_version (State {versions, ...}) (id: version_id) =
   4.141 +fun the_version (State {versions, ...}) (id: Document_ID.version) =
   4.142    (case Inttab.lookup versions id of
   4.143      NONE => err_undef "document version" id
   4.144    | SOME version => version);
   4.145  
   4.146 -fun delete_version (id: version_id) versions = Inttab.delete id versions
   4.147 +fun delete_version (id: Document_ID.version) versions = Inttab.delete id versions
   4.148    handle Inttab.UNDEF _ => err_undef "document version" id;
   4.149  
   4.150  
   4.151  (* commands *)
   4.152  
   4.153 -fun define_command (id: command_id) name text =
   4.154 +fun define_command (id: Document_ID.command) name text =
   4.155    map_state (fn (versions, commands, execution) =>
   4.156      let
   4.157 -      val id_string = print_id id;
   4.158 +      val id_string = Document_ID.print id;
   4.159        val span = Lazy.lazy (fn () =>
   4.160          Position.setmp_thread_data (Position.id_only id_string)
   4.161            (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
   4.162 @@ -290,7 +269,7 @@
   4.163            handle Inttab.DUP dup => err_dup "command" dup;
   4.164      in (versions, commands', execution) end);
   4.165  
   4.166 -fun the_command (State {commands, ...}) (id: command_id) =
   4.167 +fun the_command (State {commands, ...}) (id: Document_ID.command) =
   4.168    (case Inttab.lookup commands id of
   4.169      NONE => err_undef "command" id
   4.170    | SOME command => command);
   4.171 @@ -300,7 +279,7 @@
   4.172  fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
   4.173    let
   4.174      val _ = member (op =) ids (#1 execution) andalso
   4.175 -      error ("Attempt to remove execution version " ^ print_id (#1 execution));
   4.176 +      error ("Attempt to remove execution version " ^ Document_ID.print (#1 execution));
   4.177  
   4.178      val versions' = fold delete_version ids versions;
   4.179      val commands' =
   4.180 @@ -451,19 +430,19 @@
   4.181            (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
   4.182          else (I, init);
   4.183  
   4.184 -      val exec_id' = new_id ();
   4.185 +      val exec_id' = Document_ID.make ();
   4.186        val eval' =
   4.187          Command.memo (fn () =>
   4.188            let
   4.189              val eval_state = exec_result (snd command_exec);
   4.190              val tr =
   4.191 -              Position.setmp_thread_data (Position.id_only (print_id exec_id'))
   4.192 +              Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id'))
   4.193                  (fn () =>
   4.194                    Command.read span
   4.195                    |> modify_init
   4.196                    |> Toplevel.put_id exec_id') ();
   4.197            in Command.eval span tr eval_state end);
   4.198 -      val prints' = if command_visible then Command.print new_id command_name eval' else [];
   4.199 +      val prints' = if command_visible then Command.print command_name eval' else [];
   4.200        val command_exec' = (command_id', (exec_id', (eval', prints')));
   4.201      in SOME (command_exec' :: execs, command_exec', init') end;
   4.202  
   4.203 @@ -472,7 +451,7 @@
   4.204      SOME (exec_id, (eval, prints)) =>
   4.205        let
   4.206          val (command_name, _) = the_command state command_id;
   4.207 -        val new_prints = Command.print new_id command_name eval;
   4.208 +        val new_prints = Command.print command_name eval;
   4.209          val prints' =
   4.210            new_prints |> map (fn new_print =>
   4.211              (case find_first (fn {name, ...} => name = #name new_print) prints of
   4.212 @@ -486,7 +465,7 @@
   4.213  
   4.214  in
   4.215  
   4.216 -fun update (old_id: version_id) (new_id: version_id) edits state =
   4.217 +fun update (old_id: Document_ID.version) (new_id: Document_ID.version) edits state =
   4.218    let
   4.219      val old_version = the_version state old_id;
   4.220      val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
   4.221 @@ -547,7 +526,8 @@
   4.222                            then SOME res
   4.223                            else SOME (id0 :: res)) node0 [];
   4.224  
   4.225 -                    val last_exec = if command_id' = no_id then NONE else SOME command_id';
   4.226 +                    val last_exec =
   4.227 +                      if command_id' = Document_ID.none then NONE else SOME command_id';
   4.228                      val result =
   4.229                        if is_some (after_entry node last_exec) then NONE
   4.230                        else SOME eval';

     5.1 --- a/src/Pure/PIDE/document.scala	Fri Jul 05 14:09:06 2013 +0200
     5.2 +++ b/src/Pure/PIDE/document.scala	Fri Jul 05 15:38:03 2013 +0200
     5.3 @@ -13,20 +13,6 @@
     5.4  
     5.5  object Document
     5.6  {
     5.7 -  /* formal identifiers */
     5.8 -
     5.9 -  type ID = Long
    5.10 -  val ID = Properties.Value.Long
    5.11 -
    5.12 -  type Version_ID = ID
    5.13 -  type Command_ID = ID
    5.14 -  type Exec_ID = ID
    5.15 -
    5.16 -  val no_id: ID = 0
    5.17 -  val new_id = Counter()
    5.18 -
    5.19 -
    5.20 -
    5.21    /** document structure **/
    5.22  
    5.23    /* individual nodes */
    5.24 @@ -202,15 +188,15 @@
    5.25      val init: Version = new Version()
    5.26  
    5.27      def make(syntax: Outer_Syntax, nodes: Nodes): Version =
    5.28 -      new Version(new_id(), syntax, nodes)
    5.29 +      new Version(Document_ID.make(), syntax, nodes)
    5.30    }
    5.31  
    5.32    final class Version private(
    5.33 -    val id: Version_ID = no_id,
    5.34 +    val id: Document_ID.Version = Document_ID.none,
    5.35      val syntax: Outer_Syntax = Outer_Syntax.empty,
    5.36      val nodes: Nodes = Nodes.empty)
    5.37    {
    5.38 -    def is_init: Boolean = id == no_id
    5.39 +    def is_init: Boolean = id == Document_ID.none
    5.40    }
    5.41  
    5.42  
    5.43 @@ -289,7 +275,7 @@
    5.44        result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
    5.45    }
    5.46  
    5.47 -  type Assign = List[(Document.Command_ID, List[Document.Exec_ID])]  // exec state assignment
    5.48 +  type Assign = List[(Document_ID.Command, List[Document_ID.Exec])]  // exec state assignment
    5.49  
    5.50    object State
    5.51    {
    5.52 @@ -301,13 +287,14 @@
    5.53      }
    5.54  
    5.55      final class Assignment private(
    5.56 -      val command_execs: Map[Command_ID, List[Exec_ID]] = Map.empty,
    5.57 +      val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
    5.58        val is_finished: Boolean = false)
    5.59      {
    5.60        def check_finished: Assignment = { require(is_finished); this }
    5.61        def unfinished: Assignment = new Assignment(command_execs, false)
    5.62  
    5.63 -      def assign(add_command_execs: List[(Command_ID, List[Exec_ID])]): Assignment =
    5.64 +      def assign(
    5.65 +        add_command_execs: List[(Document_ID.Command, List[Document_ID.Exec])]): Assignment =
    5.66        {
    5.67          require(!is_finished)
    5.68          val command_execs1 =
    5.69 @@ -324,10 +311,10 @@
    5.70    }
    5.71  
    5.72    final case class State private(
    5.73 -    val versions: Map[Version_ID, Version] = Map.empty,
    5.74 -    val commands: Map[Command_ID, Command.State] = Map.empty,  // static markup from define_command
    5.75 -    val execs: Map[Exec_ID, Command.State] = Map.empty,  // dynamic markup from execution
    5.76 -    val assignments: Map[Version_ID, State.Assignment] = Map.empty,
    5.77 +    val versions: Map[Document_ID.Version, Version] = Map.empty,
    5.78 +    val commands: Map[Document_ID.Command, Command.State] = Map.empty,  // static markup from define_command
    5.79 +    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,  // dynamic markup from execution
    5.80 +    val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
    5.81      val history: History = History.init)
    5.82    {
    5.83      private def fail[A]: A = throw new State.Fail(this)
    5.84 @@ -345,9 +332,9 @@
    5.85        copy(commands = commands + (id -> command.init_state))
    5.86      }
    5.87  
    5.88 -    def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
    5.89 +    def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
    5.90  
    5.91 -    def find_command(version: Version, id: ID): Option[(Node, Command)] =
    5.92 +    def find_command(version: Version, id: Document_ID.ID): Option[(Node, Command)] =
    5.93        commands.get(id) orElse execs.get(id) match {
    5.94          case None => None
    5.95          case Some(st) =>
    5.96 @@ -356,13 +343,13 @@
    5.97            Some((node, command))
    5.98        }
    5.99  
   5.100 -    def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
   5.101 -    def the_read_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
   5.102 -    def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
   5.103 +    def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
   5.104 +    def the_read_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
   5.105 +    def the_exec_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
   5.106      def the_assignment(version: Version): State.Assignment =
   5.107        assignments.getOrElse(version.id, fail)
   5.108  
   5.109 -    def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
   5.110 +    def accumulate(id: Document_ID.ID, message: XML.Elem): (Command.State, State) =
   5.111        execs.get(id) match {
   5.112          case Some(st) =>
   5.113            val new_st = st + (id, message)
   5.114 @@ -376,7 +363,7 @@
   5.115            }
   5.116        }
   5.117  
   5.118 -    def assign(id: Version_ID, command_execs: Assign = Nil): (List[Command], State) =
   5.119 +    def assign(id: Document_ID.Version, command_execs: Assign = Nil): (List[Command], State) =
   5.120      {
   5.121        val version = the_version(id)
   5.122  
   5.123 @@ -437,12 +424,12 @@
   5.124        }
   5.125      }
   5.126  
   5.127 -    def removed_versions(removed: List[Version_ID]): State =
   5.128 +    def removed_versions(removed: List[Document_ID.Version]): State =
   5.129      {
   5.130        val versions1 = versions -- removed
   5.131        val assignments1 = assignments -- removed
   5.132 -      var commands1 = Map.empty[Command_ID, Command.State]
   5.133 -      var execs1 = Map.empty[Exec_ID, Command.State]
   5.134 +      var commands1 = Map.empty[Document_ID.Command, Command.State]
   5.135 +      var execs1 = Map.empty[Document_ID.Exec, Command.State]
   5.136        for {
   5.137          (version_id, version) <- versions1.iterator
   5.138          command_execs = assignments1(version_id).command_execs

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/PIDE/document_id.ML	Fri Jul 05 15:38:03 2013 +0200
     6.3 @@ -0,0 +1,36 @@
     6.4 +(*  Title:      Pure/PIDE/document_id.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Unique identifiers for document structure.
     6.8 +
     6.9 +NB: ML ticks forwards > 0, JVM ticks backwards < 0.
    6.10 +*)
    6.11 +
    6.12 +signature DOCUMENT_ID =
    6.13 +sig
    6.14 +  type id = int
    6.15 +  type version = id
    6.16 +  type command = id
    6.17 +  type exec = id
    6.18 +  val none: id
    6.19 +  val make: unit -> id
    6.20 +  val parse: string -> id
    6.21 +  val print: id -> string
    6.22 +end;
    6.23 +
    6.24 +structure Document_ID: DOCUMENT_ID =
    6.25 +struct
    6.26 +
    6.27 +type id = int;
    6.28 +type version = id;
    6.29 +type command = id;
    6.30 +type exec = id;
    6.31 +
    6.32 +val none = 0;
    6.33 +val make = Synchronized.counter ();
    6.34 +
    6.35 +val parse = Markup.parse_int;
    6.36 +val print = Markup.print_int;
    6.37 +
    6.38 +end;
    6.39 +

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/PIDE/document_id.scala	Fri Jul 05 15:38:03 2013 +0200
     7.3 @@ -0,0 +1,24 @@
     7.4 +/*  Title:      Pure/PIDE/document_id.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Unique identifiers for document structure.
     7.8 +
     7.9 +NB: ML ticks forwards > 0, JVM ticks backwards < 0.
    7.10 +*/
    7.11 +
    7.12 +package isabelle
    7.13 +
    7.14 +
    7.15 +object Document_ID
    7.16 +{
    7.17 +  type ID = Long
    7.18 +  val ID = Properties.Value.Long
    7.19 +
    7.20 +  type Version = ID
    7.21 +  type Command = ID
    7.22 +  type Exec = ID
    7.23 +
    7.24 +  val none: ID = 0
    7.25 +  val make = Counter()
    7.26 +}
    7.27 +

     8.1 --- a/src/Pure/PIDE/protocol.ML	Fri Jul 05 14:09:06 2013 +0200
     8.2 +++ b/src/Pure/PIDE/protocol.ML	Fri Jul 05 15:38:03 2013 +0200
     8.3 @@ -10,7 +10,7 @@
     8.4  val _ =
     8.5    Isabelle_Process.protocol_command "Document.define_command"
     8.6      (fn [id, name, text] =>
     8.7 -      Document.change_state (Document.define_command (Document.parse_id id) name text));
     8.8 +      Document.change_state (Document.define_command (Document_ID.parse id) name text));
     8.9  
    8.10  val _ =
    8.11    Isabelle_Process.protocol_command "Document.discontinue_execution"
    8.12 @@ -26,8 +26,8 @@
    8.13        let
    8.14          val _ = Document.cancel_execution state;
    8.15  
    8.16 -        val old_id = Document.parse_id old_id_string;
    8.17 -        val new_id = Document.parse_id new_id_string;
    8.18 +        val old_id = Document_ID.parse old_id_string;
    8.19 +        val new_id = Document_ID.parse new_id_string;
    8.20          val edits =
    8.21            YXML.parse_body edits_yxml |>
    8.22              let open XML.Decode in

     9.1 --- a/src/Pure/PIDE/protocol.scala	Fri Jul 05 14:09:06 2013 +0200
     9.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Jul 05 15:38:03 2013 +0200
     9.3 @@ -13,7 +13,7 @@
     9.4  
     9.5    object Assign
     9.6    {
     9.7 -    def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
     9.8 +    def unapply(text: String): Option[(Document_ID.Version, Document.Assign)] =
     9.9        try {
    9.10          import XML.Decode._
    9.11          val body = YXML.parse_body(text)
    9.12 @@ -27,7 +27,7 @@
    9.13  
    9.14    object Removed
    9.15    {
    9.16 -    def unapply(text: String): Option[List[Document.Version_ID]] =
    9.17 +    def unapply(text: String): Option[List[Document_ID.Version]] =
    9.18        try {
    9.19          import XML.Decode._
    9.20          Some(list(long)(YXML.parse_body(text)))
    9.21 @@ -86,7 +86,7 @@
    9.22  
    9.23    object Command_Timing
    9.24    {
    9.25 -    def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
    9.26 +    def unapply(props: Properties.T): Option[(Document_ID.ID, isabelle.Timing)] =
    9.27        props match {
    9.28          case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
    9.29            (args, args) match {
    9.30 @@ -233,7 +233,7 @@
    9.31  
    9.32    object Dialog_Args
    9.33    {
    9.34 -    def unapply(props: Properties.T): Option[(Document.ID, Long, String)] =
    9.35 +    def unapply(props: Properties.T): Option[(Document_ID.ID, Long, String)] =
    9.36        (props, props, props) match {
    9.37          case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
    9.38            Some((id, serial, result))
    9.39 @@ -243,7 +243,7 @@
    9.40  
    9.41    object Dialog
    9.42    {
    9.43 -    def unapply(tree: XML.Tree): Option[(Document.ID, Long, String)] =
    9.44 +    def unapply(tree: XML.Tree): Option[(Document_ID.ID, Long, String)] =
    9.45        tree match {
    9.46          case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
    9.47            Some((id, serial, result))
    9.48 @@ -253,7 +253,7 @@
    9.49  
    9.50    object Dialog_Result
    9.51    {
    9.52 -    def apply(id: Document.ID, serial: Long, result: String): XML.Elem =
    9.53 +    def apply(id: Document_ID.ID, serial: Long, result: String): XML.Elem =
    9.54      {
    9.55        val props = Position.Id(id) ::: Markup.Serial(serial)
    9.56        XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
    9.57 @@ -309,7 +309,7 @@
    9.58  
    9.59    def define_command(command: Command): Unit =
    9.60      input("Document.define_command",
    9.61 -      Document.ID(command.id), encode(command.name), encode(command.source))
    9.62 +      Document_ID.ID(command.id), encode(command.name), encode(command.source))
    9.63  
    9.64  
    9.65    /* document versions */
    9.66 @@ -318,7 +318,7 @@
    9.67  
    9.68    def cancel_execution() { input("Document.cancel_execution") }
    9.69  
    9.70 -  def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
    9.71 +  def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
    9.72      edits: List[Document.Edit_Command])
    9.73    {
    9.74      val edits_yxml =
    9.75 @@ -346,7 +346,7 @@
    9.76          pair(string, encode_edit(name))(name.node, edit)
    9.77        })
    9.78        YXML.string_of_body(encode_edits(edits)) }
    9.79 -    input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
    9.80 +    input("Document.update", Document_ID.ID(old_id), Document_ID.ID(new_id), edits_yxml)
    9.81    }
    9.82  
    9.83    def remove_versions(versions: List[Document.Version])

    10.1 --- a/src/Pure/ROOT	Fri Jul 05 14:09:06 2013 +0200
    10.2 +++ b/src/Pure/ROOT	Fri Jul 05 15:38:03 2013 +0200
    10.3 @@ -152,6 +152,7 @@
    10.4      "PIDE/active.ML"
    10.5      "PIDE/command.ML"
    10.6      "PIDE/document.ML"
    10.7 +    "PIDE/document_id.ML"
    10.8      "PIDE/markup.ML"
    10.9      "PIDE/protocol.ML"
   10.10      "PIDE/xml.ML"

    11.1 --- a/src/Pure/ROOT.ML	Fri Jul 05 14:09:06 2013 +0200
    11.2 +++ b/src/Pure/ROOT.ML	Fri Jul 05 15:38:03 2013 +0200
    11.3 @@ -265,6 +265,7 @@
    11.4  use "Isar/outer_syntax.ML";
    11.5  use "General/graph_display.ML";
    11.6  use "Thy/present.ML";
    11.7 +use "PIDE/document_id.ML";
    11.8  use "PIDE/command.ML";
    11.9  use "Thy/thy_load.ML";
   11.10  use "Thy/thy_info.ML";

    12.1 --- a/src/Pure/System/session.scala	Fri Jul 05 14:09:06 2013 +0200
    12.2 +++ b/src/Pure/System/session.scala	Fri Jul 05 15:38:03 2013 +0200
    12.3 @@ -26,7 +26,7 @@
    12.4    case class Global_Options(options: Options)
    12.5    case object Caret_Focus
    12.6    case class Raw_Edits(edits: List[Document.Edit_Text])
    12.7 -  case class Dialog_Result(id: Document.ID, serial: Long, result: String)
    12.8 +  case class Dialog_Result(id: Document_ID.ID, serial: Long, result: String)
    12.9    case class Commands_Changed(
   12.10      assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command])
   12.11  
   12.12 @@ -374,7 +374,7 @@
   12.13            System.err.println("Ignoring prover output: " + output.message.toString)
   12.14        }
   12.15  
   12.16 -      def accumulate(state_id: Document.ID, message: XML.Elem)
   12.17 +      def accumulate(state_id: Document_ID.ID, message: XML.Elem)
   12.18        {
   12.19          try {
   12.20            val st = global_state >>> (_.accumulate(state_id, message))
   12.21 @@ -548,6 +548,6 @@
   12.22    def update_options(options: Options)
   12.23    { session_actor !? Update_Options(options) }
   12.24  
   12.25 -  def dialog_result(id: Document.ID, serial: Long, result: String)
   12.26 +  def dialog_result(id: Document_ID.ID, serial: Long, result: String)
   12.27    { session_actor ! Session.Dialog_Result(id, serial, result) }
   12.28  }

    13.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Jul 05 14:09:06 2013 +0200
    13.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Jul 05 15:38:03 2013 +0200
    13.3 @@ -68,7 +68,7 @@
    13.4        /* result structure */
    13.5  
    13.6        val spans = parse_spans(syntax.scan(text))
    13.7 -      spans.foreach(span => add(Command(Document.no_id, node_name, span)))
    13.8 +      spans.foreach(span => add(Command(Document_ID.none, node_name, span)))
    13.9        result()
   13.10      }
   13.11    }
   13.12 @@ -225,7 +225,7 @@
   13.13          commands
   13.14        case cmd :: _ =>
   13.15          val hook = commands.prev(cmd)
   13.16 -        val inserted = spans2.map(span => Command(Document.new_id(), name, span))
   13.17 +        val inserted = spans2.map(span => Command(Document_ID.make(), name, span))
   13.18          (commands /: cmds2)(_ - _).append_after(hook, inserted)
   13.19      }
   13.20    }

    14.1 --- a/src/Pure/build-jars	Fri Jul 05 14:09:06 2013 +0200
    14.2 +++ b/src/Pure/build-jars	Fri Jul 05 15:38:03 2013 +0200
    14.3 @@ -33,6 +33,7 @@
    14.4    Isar/token.scala
    14.5    PIDE/command.scala
    14.6    PIDE/document.scala
    14.7 +  PIDE/document_id.scala
    14.8    PIDE/markup.scala
    14.9    PIDE/markup_tree.scala
   14.10    PIDE/protocol.scala

    15.1 --- a/src/Tools/jEdit/src/active.scala	Fri Jul 05 14:09:06 2013 +0200
    15.2 +++ b/src/Tools/jEdit/src/active.scala	Fri Jul 05 15:38:03 2013 +0200
    15.3 @@ -26,7 +26,7 @@
    15.4            val buffer = model.buffer
    15.5            val snapshot = model.snapshot()
    15.6  
    15.7 -          def try_replace_command(exec_id: Document.ID, s: String)
    15.8 +          def try_replace_command(exec_id: Document_ID.ID, s: String)
    15.9            {
   15.10              snapshot.state.execs.get(exec_id).map(_.command) match {
   15.11                case Some(command) =>

    16.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jul 05 14:09:06 2013 +0200
    16.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Jul 05 15:38:03 2013 +0200
    16.3 @@ -24,7 +24,7 @@
    16.4    private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
    16.5      formatted_body: XML.Body): (String, Document.State) =
    16.6    {
    16.7 -    val command = Command.rich_text(Document.new_id(), base_results, formatted_body)
    16.8 +    val command = Command.rich_text(Document_ID.make(), base_results, formatted_body)
    16.9      val node_name = command.node_name
   16.10      val edits: List[Document.Edit_Text] =
   16.11        List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
   16.12 @@ -38,7 +38,7 @@
   16.13      val state1 =
   16.14        state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
   16.15          .define_version(version1, state0.the_assignment(version0))
   16.16 -        .assign(version1.id, List(command.id -> List(Document.new_id())))._2
   16.17 +        .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
   16.18  
   16.19      (command.source, state1)
   16.20    }

    17.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Jul 05 14:09:06 2013 +0200
    17.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Jul 05 15:38:03 2013 +0200
    17.3 @@ -290,7 +290,7 @@
    17.4  
    17.5            case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
    17.6            if !body.isEmpty =>
    17.7 -            val entry: Command.Results.Entry = (Document.new_id(), msg)
    17.8 +            val entry: Command.Results.Entry = (Document_ID.make(), msg)
    17.9              Text.Info(snapshot.convert(info_range), entry) :: msgs
   17.10          }).toList.flatMap(_.info)
   17.11      if (results.isEmpty) None