explicit module Document_ID as source of globally unique identifiers across ML/Scala;
--- a/src/Pure/Concurrent/synchronized.ML Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Fri Jul 05 15:38:03 2013 +0200
@@ -69,6 +69,7 @@
(* unique identifiers > 0 *)
+(*NB: ML ticks forwards, JVM ticks backwards*)
fun counter () =
let
val counter = var "counter" (0: int);
--- a/src/Pure/PIDE/command.ML Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/command.ML Fri Jul 05 15:38:03 2013 +0200
@@ -23,8 +23,8 @@
val no_eval: eval
val eval: span -> Toplevel.transition -> eval_state -> eval_state
type print_fn = Toplevel.transition -> Toplevel.state -> unit
- type print = {name: string, pri: int, exec_id: int, print: unit memo}
- val print: (unit -> int) -> string -> eval -> print list
+ type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo}
+ val print: string -> eval -> print list
val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
end;
@@ -175,7 +175,7 @@
(* print *)
-type print = {name: string, pri: int, exec_id: int, print: unit memo};
+type print = {name: string, pri: int, exec_id: Document_ID.exec, print: unit memo};
type print_fn = Toplevel.transition -> Toplevel.state -> unit;
local
@@ -192,13 +192,13 @@
in
-fun print new_id command_name eval =
+fun print command_name eval =
rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
(case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
Exn.Res NONE => NONE
| Exn.Res (SOME print_fn) =>
let
- val exec_id = new_id ();
+ val exec_id = Document_ID.make ();
fun body () =
let
val {failed, command, state = st', ...} = memo_result eval;
@@ -207,7 +207,7 @@
in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
| Exn.Exn exn =>
let
- val exec_id = new_id ();
+ val exec_id = Document_ID.make ();
fun body () =
let
val {command, ...} = memo_result eval;
--- a/src/Pure/PIDE/command.scala Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/command.scala Fri Jul 05 15:38:03 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, message: XML.Elem): State =
+ def + (alt_id: Document_ID.ID, message: XML.Elem): State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
@@ -136,7 +136,7 @@
type Span = List[Token]
def apply(
- id: Document.Command_ID,
+ id: Document_ID.Command,
node_name: Document.Node.Name,
span: Span,
results: Results = Results.empty,
@@ -160,16 +160,16 @@
new Command(id, node_name, span1.toList, source, results, markup)
}
- val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
+ val empty = Command(Document_ID.none, Document.Node.Name.empty, Nil)
- def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree)
+ def unparsed(id: Document_ID.Command, source: String, results: Results, markup: Markup_Tree)
: Command =
Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
def unparsed(source: String): Command =
- unparsed(Document.no_id, source, Results.empty, Markup_Tree.empty)
+ unparsed(Document_ID.none, source, Results.empty, Markup_Tree.empty)
- def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
+ def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command =
{
val text = XML.content(body)
val markup = Markup_Tree.from_XML(body)
@@ -200,7 +200,7 @@
final class Command private(
- val id: Document.Command_ID,
+ val id: Document_ID.Command,
val node_name: Document.Node.Name,
val span: Command.Span,
val source: String,
@@ -209,7 +209,7 @@
{
/* classification */
- def is_undefined: Boolean = id == Document.no_id
+ def is_undefined: Boolean = id == Document_ID.none
val is_unparsed: Boolean = span.exists(_.is_unparsed)
val is_unfinished: Boolean = span.exists(_.is_unfinished)
--- a/src/Pure/PIDE/document.ML Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/document.ML Fri Jul 05 15:38:03 2013 +0200
@@ -7,31 +7,23 @@
signature DOCUMENT =
sig
- type id = int
- type version_id = id
- type command_id = id
- type exec_id = id
- val no_id: id
- val new_id: unit -> id
- val parse_id: string -> id
- val print_id: id -> string
type node_header = string * Thy_Header.header * string list
datatype node_edit =
Clear | (* FIXME unused !? *)
- Edits of (command_id option * command_id option) list |
+ Edits of (Document_ID.command option * Document_ID.command option) list |
Deps of node_header |
- Perspective of command_id list
+ Perspective of Document_ID.command list
type edit = string * node_edit
type state
val init_state: state
- val define_command: command_id -> string -> string -> state -> state
- val remove_versions: version_id list -> state -> state
+ val define_command: Document_ID.command -> string -> string -> state -> state
+ val remove_versions: Document_ID.version list -> state -> state
val discontinue_execution: state -> unit
val cancel_execution: state -> unit
val start_execution: state -> unit
val timing: bool Unsynchronized.ref
- val update: version_id -> version_id -> edit list -> state ->
- (command_id * exec_id list) list * state
+ val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
+ (Document_ID.command * Document_ID.exec list) list * state
val state: unit -> state
val change_state: (state -> state) -> unit
end;
@@ -39,27 +31,10 @@
structure Document: DOCUMENT =
struct
-(* unique identifiers *)
-
-type id = int;
-type version_id = id;
-type command_id = id;
-type exec_id = id;
-
-val no_id = 0;
-val new_id = Synchronized.counter ();
-
-val parse_id = Markup.parse_int;
-val print_id = Markup.print_int;
-
-fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id);
-fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
-
-
(* command execution *)
-type exec = exec_id * (Command.eval * Command.print list); (*eval/print process*)
-val no_exec: exec = (no_id, (Command.no_eval, []));
+type exec = Document_ID.exec * (Command.eval * Command.print list); (*eval/print process*)
+val no_exec: exec = (Document_ID.none, (Command.no_eval, []));
fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
@@ -74,9 +49,12 @@
(** document structure **)
+fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id);
+fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id);
+
type node_header = string * Thy_Header.header * string list;
-type perspective = Inttab.set * command_id option;
-structure Entries = Linear_Set(type key = command_id val ord = int_ord);
+type perspective = Inttab.set * Document_ID.command option;
+structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
abstype node = Node of
{header: node_header, (*master directory, theory header, errors*)
@@ -156,9 +134,9 @@
datatype node_edit =
Clear |
- Edits of (command_id option * command_id option) list |
+ Edits of (Document_ID.command option * Document_ID.command option) list |
Deps of node_header |
- Perspective of command_id list;
+ Perspective of Document_ID.command list;
type edit = string * node_edit;
@@ -175,7 +153,7 @@
| SOME (exec, _) => exec);
fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
- | the_default_entry _ NONE = (no_id, no_exec);
+ | the_default_entry _ NONE = (Document_ID.none, no_exec);
fun update_entry id exec =
map_entries (Entries.update (id, exec));
@@ -237,7 +215,8 @@
abstype state = State of
{versions: version Inttab.table, (*version_id -> document content*)
commands: (string * Token.T list lazy) Inttab.table, (*command_id -> named span*)
- execution: version_id * Future.group * bool Unsynchronized.ref} (*current execution process*)
+ execution:
+ Document_ID.version * Future.group * bool Unsynchronized.ref} (*current execution process*)
with
fun make_state (versions, commands, execution) =
@@ -247,15 +226,15 @@
make_state (f (versions, commands, execution));
val init_state =
- make_state (Inttab.make [(no_id, empty_version)], Inttab.empty,
- (no_id, Future.new_group NONE, Unsynchronized.ref false));
+ make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty,
+ (Document_ID.none, Future.new_group NONE, Unsynchronized.ref false));
fun execution_of (State {execution, ...}) = execution;
(* document versions *)
-fun define_version (id: version_id) version =
+fun define_version (id: Document_ID.version) version =
map_state (fn (versions, commands, _) =>
let
val versions' = Inttab.update_new (id, version) versions
@@ -263,21 +242,21 @@
val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
in (versions', commands, execution') end);
-fun the_version (State {versions, ...}) (id: version_id) =
+fun the_version (State {versions, ...}) (id: Document_ID.version) =
(case Inttab.lookup versions id of
NONE => err_undef "document version" id
| SOME version => version);
-fun delete_version (id: version_id) versions = Inttab.delete id versions
+fun delete_version (id: Document_ID.version) versions = Inttab.delete id versions
handle Inttab.UNDEF _ => err_undef "document version" id;
(* commands *)
-fun define_command (id: command_id) name text =
+fun define_command (id: Document_ID.command) name text =
map_state (fn (versions, commands, execution) =>
let
- val id_string = print_id id;
+ val id_string = Document_ID.print id;
val span = Lazy.lazy (fn () =>
Position.setmp_thread_data (Position.id_only id_string)
(fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
@@ -290,7 +269,7 @@
handle Inttab.DUP dup => err_dup "command" dup;
in (versions, commands', execution) end);
-fun the_command (State {commands, ...}) (id: command_id) =
+fun the_command (State {commands, ...}) (id: Document_ID.command) =
(case Inttab.lookup commands id of
NONE => err_undef "command" id
| SOME command => command);
@@ -300,7 +279,7 @@
fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
let
val _ = member (op =) ids (#1 execution) andalso
- error ("Attempt to remove execution version " ^ print_id (#1 execution));
+ error ("Attempt to remove execution version " ^ Document_ID.print (#1 execution));
val versions' = fold delete_version ids versions;
val commands' =
@@ -451,19 +430,19 @@
(Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
else (I, init);
- val exec_id' = new_id ();
+ val exec_id' = Document_ID.make ();
val eval' =
Command.memo (fn () =>
let
val eval_state = exec_result (snd command_exec);
val tr =
- Position.setmp_thread_data (Position.id_only (print_id exec_id'))
+ Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id'))
(fn () =>
Command.read span
|> modify_init
|> Toplevel.put_id exec_id') ();
in Command.eval span tr eval_state end);
- val prints' = if command_visible then Command.print new_id command_name eval' else [];
+ val prints' = if command_visible then Command.print command_name eval' else [];
val command_exec' = (command_id', (exec_id', (eval', prints')));
in SOME (command_exec' :: execs, command_exec', init') end;
@@ -472,7 +451,7 @@
SOME (exec_id, (eval, prints)) =>
let
val (command_name, _) = the_command state command_id;
- val new_prints = Command.print new_id command_name eval;
+ val new_prints = Command.print command_name eval;
val prints' =
new_prints |> map (fn new_print =>
(case find_first (fn {name, ...} => name = #name new_print) prints of
@@ -486,7 +465,7 @@
in
-fun update (old_id: version_id) (new_id: version_id) edits state =
+fun update (old_id: Document_ID.version) (new_id: Document_ID.version) edits state =
let
val old_version = the_version state old_id;
val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
@@ -547,7 +526,8 @@
then SOME res
else SOME (id0 :: res)) node0 [];
- val last_exec = if command_id' = no_id then NONE else SOME command_id';
+ val last_exec =
+ if command_id' = Document_ID.none then NONE else SOME command_id';
val result =
if is_some (after_entry node last_exec) then NONE
else SOME eval';
--- a/src/Pure/PIDE/document.scala Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/document.scala Fri Jul 05 15:38:03 2013 +0200
@@ -13,20 +13,6 @@
object Document
{
- /* formal identifiers */
-
- type ID = Long
- val ID = Properties.Value.Long
-
- type Version_ID = ID
- type Command_ID = ID
- type Exec_ID = ID
-
- val no_id: ID = 0
- val new_id = Counter()
-
-
-
/** document structure **/
/* individual nodes */
@@ -202,15 +188,15 @@
val init: Version = new Version()
def make(syntax: Outer_Syntax, nodes: Nodes): Version =
- new Version(new_id(), syntax, nodes)
+ new Version(Document_ID.make(), syntax, nodes)
}
final class Version private(
- val id: Version_ID = no_id,
+ val id: Document_ID.Version = Document_ID.none,
val syntax: Outer_Syntax = Outer_Syntax.empty,
val nodes: Nodes = Nodes.empty)
{
- def is_init: Boolean = id == no_id
+ def is_init: Boolean = id == Document_ID.none
}
@@ -289,7 +275,7 @@
result: Command.State => PartialFunction[Text.Markup, A]): Stream[Text.Info[A]]
}
- type Assign = List[(Document.Command_ID, List[Document.Exec_ID])] // exec state assignment
+ type Assign = List[(Document_ID.Command, List[Document_ID.Exec])] // exec state assignment
object State
{
@@ -301,13 +287,14 @@
}
final class Assignment private(
- val command_execs: Map[Command_ID, List[Exec_ID]] = Map.empty,
+ val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty,
val is_finished: Boolean = false)
{
def check_finished: Assignment = { require(is_finished); this }
def unfinished: Assignment = new Assignment(command_execs, false)
- def assign(add_command_execs: List[(Command_ID, List[Exec_ID])]): Assignment =
+ def assign(
+ add_command_execs: List[(Document_ID.Command, List[Document_ID.Exec])]): Assignment =
{
require(!is_finished)
val command_execs1 =
@@ -324,10 +311,10 @@
}
final case class State private(
- val versions: Map[Version_ID, Version] = Map.empty,
- val commands: Map[Command_ID, Command.State] = Map.empty, // static markup from define_command
- val execs: Map[Exec_ID, Command.State] = Map.empty, // dynamic markup from execution
- val assignments: Map[Version_ID, State.Assignment] = Map.empty,
+ val versions: Map[Document_ID.Version, Version] = Map.empty,
+ val commands: Map[Document_ID.Command, Command.State] = Map.empty, // static markup from define_command
+ val execs: Map[Document_ID.Exec, Command.State] = Map.empty, // dynamic markup from execution
+ val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
val history: History = History.init)
{
private def fail[A]: A = throw new State.Fail(this)
@@ -345,9 +332,9 @@
copy(commands = commands + (id -> command.init_state))
}
- def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
+ def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id)
- def find_command(version: Version, id: ID): Option[(Node, Command)] =
+ def find_command(version: Version, id: Document_ID.ID): Option[(Node, Command)] =
commands.get(id) orElse execs.get(id) match {
case None => None
case Some(st) =>
@@ -356,13 +343,13 @@
Some((node, command))
}
- def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
- def the_read_state(id: Command_ID): Command.State = commands.getOrElse(id, fail)
- def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)
+ def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail)
+ def the_read_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail)
+ def the_exec_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail)
def the_assignment(version: Version): State.Assignment =
assignments.getOrElse(version.id, fail)
- def accumulate(id: ID, message: XML.Elem): (Command.State, State) =
+ def accumulate(id: Document_ID.ID, message: XML.Elem): (Command.State, State) =
execs.get(id) match {
case Some(st) =>
val new_st = st + (id, message)
@@ -376,7 +363,7 @@
}
}
- def assign(id: Version_ID, command_execs: Assign = Nil): (List[Command], State) =
+ def assign(id: Document_ID.Version, command_execs: Assign = Nil): (List[Command], State) =
{
val version = the_version(id)
@@ -437,12 +424,12 @@
}
}
- def removed_versions(removed: List[Version_ID]): State =
+ def removed_versions(removed: List[Document_ID.Version]): State =
{
val versions1 = versions -- removed
val assignments1 = assignments -- removed
- var commands1 = Map.empty[Command_ID, Command.State]
- var execs1 = Map.empty[Exec_ID, Command.State]
+ var commands1 = Map.empty[Document_ID.Command, Command.State]
+ var execs1 = Map.empty[Document_ID.Exec, Command.State]
for {
(version_id, version) <- versions1.iterator
command_execs = assignments1(version_id).command_execs
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document_id.ML Fri Jul 05 15:38:03 2013 +0200
@@ -0,0 +1,36 @@
+(* Title: Pure/PIDE/document_id.ML
+ Author: Makarius
+
+Unique identifiers for document structure.
+
+NB: ML ticks forwards > 0, JVM ticks backwards < 0.
+*)
+
+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
+end;
+
+structure Document_ID: DOCUMENT_ID =
+struct
+
+type id = int;
+type version = id;
+type command = id;
+type exec = id;
+
+val none = 0;
+val make = Synchronized.counter ();
+
+val parse = Markup.parse_int;
+val print = Markup.print_int;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/document_id.scala Fri Jul 05 15:38:03 2013 +0200
@@ -0,0 +1,24 @@
+/* Title: Pure/PIDE/document_id.scala
+ Author: Makarius
+
+Unique identifiers for document structure.
+
+NB: ML ticks forwards > 0, JVM ticks backwards < 0.
+*/
+
+package isabelle
+
+
+object Document_ID
+{
+ type ID = Long
+ val ID = Properties.Value.Long
+
+ type Version = ID
+ type Command = ID
+ type Exec = ID
+
+ val none: ID = 0
+ val make = Counter()
+}
+
--- a/src/Pure/PIDE/protocol.ML Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Jul 05 15:38:03 2013 +0200
@@ -10,7 +10,7 @@
val _ =
Isabelle_Process.protocol_command "Document.define_command"
(fn [id, name, text] =>
- Document.change_state (Document.define_command (Document.parse_id id) name text));
+ Document.change_state (Document.define_command (Document_ID.parse id) name text));
val _ =
Isabelle_Process.protocol_command "Document.discontinue_execution"
@@ -26,8 +26,8 @@
let
val _ = Document.cancel_execution state;
- val old_id = Document.parse_id old_id_string;
- val new_id = Document.parse_id new_id_string;
+ val old_id = Document_ID.parse old_id_string;
+ val new_id = Document_ID.parse new_id_string;
val edits =
YXML.parse_body edits_yxml |>
let open XML.Decode in
--- a/src/Pure/PIDE/protocol.scala Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Jul 05 15:38:03 2013 +0200
@@ -13,7 +13,7 @@
object Assign
{
- def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
+ def unapply(text: String): Option[(Document_ID.Version, Document.Assign)] =
try {
import XML.Decode._
val body = YXML.parse_body(text)
@@ -27,7 +27,7 @@
object Removed
{
- def unapply(text: String): Option[List[Document.Version_ID]] =
+ def unapply(text: String): Option[List[Document_ID.Version]] =
try {
import XML.Decode._
Some(list(long)(YXML.parse_body(text)))
@@ -86,7 +86,7 @@
object Command_Timing
{
- def unapply(props: Properties.T): Option[(Document.ID, isabelle.Timing)] =
+ def unapply(props: Properties.T): Option[(Document_ID.ID, 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, Long, String)] =
+ def unapply(props: Properties.T): Option[(Document_ID.ID, 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, Long, String)] =
+ def unapply(tree: XML.Tree): Option[(Document_ID.ID, 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, serial: Long, result: String): XML.Elem =
+ def apply(id: Document_ID.ID, 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(command.id), encode(command.name), encode(command.source))
+ Document_ID.ID(command.id), encode(command.name), encode(command.source))
/* document versions */
@@ -318,7 +318,7 @@
def cancel_execution() { input("Document.cancel_execution") }
- def update(old_id: Document.Version_ID, new_id: Document.Version_ID,
+ def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
edits: List[Document.Edit_Command])
{
val edits_yxml =
@@ -346,7 +346,7 @@
pair(string, encode_edit(name))(name.node, edit)
})
YXML.string_of_body(encode_edits(edits)) }
- input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
+ input("Document.update", Document_ID.ID(old_id), Document_ID.ID(new_id), edits_yxml)
}
def remove_versions(versions: List[Document.Version])
--- a/src/Pure/ROOT Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/ROOT Fri Jul 05 15:38:03 2013 +0200
@@ -152,6 +152,7 @@
"PIDE/active.ML"
"PIDE/command.ML"
"PIDE/document.ML"
+ "PIDE/document_id.ML"
"PIDE/markup.ML"
"PIDE/protocol.ML"
"PIDE/xml.ML"
--- a/src/Pure/ROOT.ML Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/ROOT.ML Fri Jul 05 15:38:03 2013 +0200
@@ -265,6 +265,7 @@
use "Isar/outer_syntax.ML";
use "General/graph_display.ML";
use "Thy/present.ML";
+use "PIDE/document_id.ML";
use "PIDE/command.ML";
use "Thy/thy_load.ML";
use "Thy/thy_info.ML";
--- a/src/Pure/System/session.scala Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/System/session.scala Fri Jul 05 15:38:03 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, serial: Long, result: String)
+ case class Dialog_Result(id: Document_ID.ID, 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, message: XML.Elem)
+ def accumulate(state_id: Document_ID.ID, 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, serial: Long, result: String)
+ def dialog_result(id: Document_ID.ID, serial: Long, result: String)
{ session_actor ! Session.Dialog_Result(id, serial, result) }
}
--- a/src/Pure/Thy/thy_syntax.scala Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Jul 05 15:38:03 2013 +0200
@@ -68,7 +68,7 @@
/* result structure */
val spans = parse_spans(syntax.scan(text))
- spans.foreach(span => add(Command(Document.no_id, node_name, span)))
+ spans.foreach(span => add(Command(Document_ID.none, node_name, span)))
result()
}
}
@@ -225,7 +225,7 @@
commands
case cmd :: _ =>
val hook = commands.prev(cmd)
- val inserted = spans2.map(span => Command(Document.new_id(), name, span))
+ val inserted = spans2.map(span => Command(Document_ID.make(), name, span))
(commands /: cmds2)(_ - _).append_after(hook, inserted)
}
}
--- a/src/Pure/build-jars Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Pure/build-jars Fri Jul 05 15:38:03 2013 +0200
@@ -33,6 +33,7 @@
Isar/token.scala
PIDE/command.scala
PIDE/document.scala
+ PIDE/document_id.scala
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
--- a/src/Tools/jEdit/src/active.scala Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Tools/jEdit/src/active.scala Fri Jul 05 15:38:03 2013 +0200
@@ -26,7 +26,7 @@
val buffer = model.buffer
val snapshot = model.snapshot()
- def try_replace_command(exec_id: Document.ID, s: String)
+ def try_replace_command(exec_id: Document_ID.ID, s: String)
{
snapshot.state.execs.get(exec_id).map(_.command) match {
case Some(command) =>
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Jul 05 15:38:03 2013 +0200
@@ -24,7 +24,7 @@
private def document_state(base_snapshot: Document.Snapshot, base_results: Command.Results,
formatted_body: XML.Body): (String, Document.State) =
{
- val command = Command.rich_text(Document.new_id(), base_results, formatted_body)
+ val command = Command.rich_text(Document_ID.make(), base_results, formatted_body)
val node_name = command.node_name
val edits: List[Document.Edit_Text] =
List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
@@ -38,7 +38,7 @@
val state1 =
state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
.define_version(version1, state0.the_assignment(version0))
- .assign(version1.id, List(command.id -> List(Document.new_id())))._2
+ .assign(version1.id, List(command.id -> List(Document_ID.make())))._2
(command.source, state1)
}
--- a/src/Tools/jEdit/src/rendering.scala Fri Jul 05 14:09:06 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Fri Jul 05 15:38:03 2013 +0200
@@ -290,7 +290,7 @@
case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
if !body.isEmpty =>
- val entry: Command.Results.Entry = (Document.new_id(), msg)
+ val entry: Command.Results.Entry = (Document_ID.make(), msg)
Text.Info(snapshot.convert(info_range), entry) :: msgs
}).toList.flatMap(_.info)
if (results.isEmpty) None