--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/counter.ML Fri Jul 05 23:17:39 2013 +0200
@@ -0,0 +1,28 @@
+(* Title: Pure/Concurrent/counter.ML
+ Author: Makarius
+
+Synchronized counter for unique identifiers > 0.
+
+NB: ML ticks forwards, JVM ticks backwards.
+*)
+
+signature COUNTER =
+sig
+ val make: unit -> unit -> int
+end;
+
+structure Counter: COUNTER =
+struct
+
+fun make () =
+ let
+ val counter = Synchronized.var "counter" (0: int);
+ fun next () =
+ Synchronized.change_result counter
+ (fn i =>
+ let val j = i + (1: int)
+ in (j, j) end);
+ in next end;
+
+end;
+
--- a/src/Pure/Concurrent/counter.scala Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/counter.scala Fri Jul 05 23:17:39 2013 +0200
@@ -13,7 +13,7 @@
object Counter
{
type ID = Long
- def apply(): Counter = new Counter
+ def make(): Counter = new Counter
}
final class Counter private
--- a/src/Pure/Concurrent/event_timer.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Fri Jul 05 23:17:39 2013 +0200
@@ -26,7 +26,7 @@
(* type request *)
-val request_counter = Synchronized.counter ();
+val request_counter = Counter.make ();
datatype request = Request of int;
fun new_request () = Request (request_counter ());
--- a/src/Pure/Concurrent/synchronized.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Fri Jul 05 23:17:39 2013 +0200
@@ -13,7 +13,6 @@
val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
val change: 'a var -> ('a -> 'a) -> unit
- val counter: unit -> unit -> int
end;
structure Synchronized: SYNCHRONIZED =
@@ -66,17 +65,4 @@
end;
-
-(* unique identifiers > 0 *)
-
-fun counter () =
- let
- val counter = var "counter" (0: int);
- fun next () =
- change_result counter
- (fn i =>
- let val j = i + (1: int)
- in (j, j) end);
- in next end;
-
end;
--- a/src/Pure/Concurrent/synchronized_sequential.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/synchronized_sequential.ML Fri Jul 05 23:17:39 2013 +0200
@@ -25,14 +25,4 @@
end;
-fun counter () =
- let
- val counter = var "counter" (0: int);
- fun next () =
- change_result counter
- (fn i =>
- let val j = i + (1: int)
- in (j, j) end);
- in next end;
-
end;
--- a/src/Pure/Concurrent/task_queue.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Fri Jul 05 23:17:39 2013 +0200
@@ -47,7 +47,7 @@
structure Task_Queue: TASK_QUEUE =
struct
-val new_id = Synchronized.counter ();
+val new_id = Counter.make ();
(** nested groups of tasks **)
--- a/src/Pure/Isar/toplevel.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML Fri Jul 05 23:17:39 2013 +0200
@@ -81,7 +81,7 @@
val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition
val skip_proof: (int -> int) -> transition -> transition
val skip_proof_to_theory: (int -> bool) -> transition -> transition
- val put_id: int -> transition -> transition
+ val exec_id: Document_ID.exec -> transition -> transition
val unknown_theory: transition -> transition
val unknown_proof: transition -> transition
val unknown_context: transition -> transition
@@ -585,8 +585,8 @@
(* runtime position *)
-fun put_id id (tr as Transition {pos, ...}) =
- position (Position.put_id (Markup.print_int id) pos) tr;
+fun exec_id id (tr as Transition {pos, ...}) =
+ position (Position.put_id (Document_ID.print id) pos) tr;
fun setmp_thread_position (Transition {pos, ...}) f x =
Position.setmp_thread_data pos f x;
--- a/src/Pure/PIDE/command.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/command.ML Fri Jul 05 23:17:39 2013 +0200
@@ -1,45 +1,33 @@
(* Title: Pure/PIDE/command.ML
Author: Makarius
-Prover command execution.
+Prover command execution: read -- eval -- print.
*)
signature COMMAND =
sig
- type span = Token.T list
- val range: span -> Position.range
- val proper_range: span -> Position.range
- type 'a memo
- val memo: (unit -> 'a) -> 'a memo
- val memo_value: 'a -> 'a memo
- val memo_eval: 'a memo -> 'a
- val memo_fork: Future.params -> 'a memo -> unit
- val memo_result: 'a memo -> 'a
- val memo_stable: 'a memo -> bool
- val read: span -> Toplevel.transition
- type eval_state =
- {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
- type eval = eval_state memo
- val no_eval: eval
- val eval: span -> Toplevel.transition -> eval_state -> eval_state
+ type eval_process
+ type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
+ val eval_result_state: eval -> Toplevel.state
+ type print_process
+ type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
+ type exec = eval * print list
+ val no_exec: exec
+ val exec_ids: exec -> Document_ID.exec list
+ val read: (unit -> theory) -> Token.T list -> Toplevel.transition
+ val eval: (unit -> theory) -> Token.T list -> eval -> eval
+ val print: string -> eval -> print list
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
val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
+ val execute: exec -> unit
+ val stable_eval: eval -> bool
+ val stable_print: print -> bool
end;
structure Command: COMMAND =
struct
-(* source *)
-
-type span = Token.T list;
-
-val range = Token.position_range_of;
-val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
-
-
-(* memo results *)
+(** memo results -- including physical interrupts! **)
datatype 'a expr =
Expr of unit -> 'a |
@@ -58,7 +46,7 @@
Synchronized.guarded_access v
(fn Result res => SOME (res, Result res)
| Expr e =>
- let val res = Exn.capture e (); (*memoing of physical interrupts!*)
+ let val res = Exn.capture e (); (*sic!*)
in SOME (res, Result res) end))
|> Exn.release;
@@ -80,14 +68,40 @@
end;
+
+(** main phases of execution **)
+
+(* basic type definitions *)
+
+type eval_state =
+ {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
+val init_eval_state =
+ {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
+
+type eval_process = eval_state memo;
+type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
+
+fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
+val eval_result_state = #state o eval_result;
+
+type print_process = unit memo;
+type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
+
+type exec = eval * print list;
+val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
+
+fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
+
+
(* read *)
-fun read span =
+fun read init span =
let
val outer_syntax = #2 (Outer_Syntax.get_syntax ());
val command_reports = Outer_Syntax.command_reports outer_syntax;
- val proper_range = Position.set_range (proper_range span);
+ val proper_range =
+ Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
val pos =
(case find_first Token.is_command span of
SOME tok => Token.position_of tok
@@ -102,8 +116,8 @@
[tr] =>
if Keyword.is_control (Toplevel.name_of tr) then
Toplevel.malformed pos "Illegal control command"
- else tr
- | [] => Toplevel.ignored (Position.set_range (range span))
+ else Toplevel.modify_init init tr
+ | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
| _ => Toplevel.malformed proper_range "Exactly one command expected")
handle ERROR msg => Toplevel.malformed proper_range msg
end;
@@ -111,14 +125,6 @@
(* eval *)
-type eval_state =
- {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
-val no_eval_state: eval_state =
- {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
-
-type eval = eval_state memo;
-val no_eval = memo_value no_eval_state;
-
local
fun run int tr st =
@@ -139,9 +145,7 @@
SOME prf => Toplevel.status tr (Proof.status_markup prf)
| NONE => ());
-in
-
-fun eval span tr ({malformed, state = st, ...}: eval_state) =
+fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
if malformed then
{failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
else
@@ -170,12 +174,24 @@
in {failed = false, malformed = malformed', command = tr, state = st'} end)
end;
+in
+
+fun eval init span eval0 =
+ let
+ val exec_id = Document_ID.make ();
+ fun process () =
+ let
+ val tr =
+ Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
+ (fn () => read init span |> Toplevel.exec_id exec_id) ();
+ in eval_state span tr (eval_result eval0) end;
+ in {exec_id = exec_id, eval_process = memo process} end;
+
end;
(* print *)
-type print = {name: string, pri: int, exec_id: int, print: unit memo};
type print_fn = Toplevel.transition -> Toplevel.state -> unit;
local
@@ -192,28 +208,28 @@
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 ();
- fun body () =
+ val exec_id = Document_ID.make ();
+ fun process () =
let
- val {failed, command, state = st', ...} = memo_result eval;
- val tr = Toplevel.put_id exec_id command;
+ val {failed, command, state = st', ...} = eval_result eval;
+ val tr = Toplevel.exec_id exec_id command;
in if failed then () else print_error tr (fn () => print_fn tr st') () end;
- in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
+ in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
| Exn.Exn exn =>
let
- val exec_id = new_id ();
- fun body () =
+ val exec_id = Document_ID.make ();
+ fun process () =
let
- val {command, ...} = memo_result eval;
- val tr = Toplevel.put_id exec_id command;
+ val {command, ...} = eval_result eval;
+ val tr = Toplevel.exec_id exec_id command;
in output_error tr exn end;
- in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
+ in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
fun print_function {name, pri} f =
Synchronized.change print_functions (fn funs =>
@@ -233,5 +249,22 @@
(Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
in if do_print then Toplevel.print_state false st' else () end));
+
+(* overall execution process *)
+
+fun execute (({eval_process, ...}, prints): exec) =
+ (memo_eval eval_process;
+ prints |> List.app (fn {name, pri, print_process, ...} =>
+ memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
+
+fun stable_goals exec_id =
+ not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
+
+fun stable_eval ({exec_id, eval_process}: eval) =
+ stable_goals exec_id andalso memo_stable eval_process;
+
+fun stable_print ({exec_id, print_process, ...}: print) =
+ stable_goals exec_id andalso memo_stable print_process;
+
end;
--- a/src/Pure/PIDE/command.scala Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/command.scala Fri Jul 05 23:17:39 2013 +0200
@@ -2,12 +2,11 @@
Author: Fabian Immler, TU Munich
Author: Makarius
-Prover commands with semantic state.
+Prover commands with accumulated results from execution.
*/
package isabelle
-import java.lang.System
import scala.collection.mutable
import scala.collection.immutable.SortedMap
@@ -75,7 +74,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.Generic, message: XML.Elem): State =
message match {
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
(this /: msgs)((state, msg) =>
@@ -84,7 +83,9 @@
state.add_status(markup)
.add_markup(Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
- case _ => System.err.println("Ignored status message: " + msg); state
+ case _ =>
+ java.lang.System.err.println("Ignored status message: " + msg)
+ state
})
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
@@ -104,7 +105,7 @@
val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
state.add_markup(info)
case _ =>
- // FIXME System.err.println("Ignored report message: " + msg)
+ // FIXME java.lang.System.err.println("Ignored report message: " + msg)
state
})
case XML.Elem(Markup(name, atts), body) =>
@@ -122,7 +123,9 @@
else st0
st1
- case _ => System.err.println("Ignored message without serial number: " + message); this
+ case _ =>
+ java.lang.System.err.println("Ignored message without serial number: " + message)
+ this
}
}
@@ -136,7 +139,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 +163,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,16 +203,16 @@
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 span: List[Token],
val source: String,
val init_results: Command.Results,
val init_markup: Markup_Tree)
{
/* 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 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/document.ML Fri Jul 05 23:17:39 2013 +0200
@@ -2,36 +2,28 @@
Author: Makarius
Document as collection of named nodes, each consisting of an editable
-list of commands, with asynchronous read/eval/print processes.
+list of commands, associated with asynchronous execution process.
*)
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,49 +31,19 @@
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, []));
-
-fun exec_ids_of ((exec_id, (_, prints)): exec) = exec_id :: map #exec_id prints;
-
-fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
-
-fun exec_run ((_, (eval, prints)): exec) =
- (Command.memo_eval eval;
- prints |> List.app (fn {name, pri, print, ...} =>
- Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
-
-
-
(** 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*)
perspective: perspective, (*visible commands, last visible command*)
- entries: exec option Entries.T * bool, (*command entries with excecutions, stable*)
+ entries: Command.exec option Entries.T * bool, (*command entries with excecutions, stable*)
result: Command.eval option} (*result of last execution*)
and version = Version of node String_Graph.T (*development graph wrt. static imports*)
with
@@ -146,6 +108,11 @@
fun set_result result =
map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
+fun finished_theory node =
+ (case Exn.capture (Command.eval_result_state o the) (get_result node) of
+ Exn.Res st => can (Toplevel.end_theory Position.none) st
+ | _ => false);
+
fun get_node nodes name = String_Graph.get_node nodes name
handle String_Graph.UNDEF _ => empty_node;
fun default_node name = String_Graph.default_node (name, empty_node);
@@ -156,9 +123,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;
@@ -174,8 +141,8 @@
NONE => err_undef "command entry" id
| 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);
+fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id))
+ | the_default_entry _ NONE = (Document_ID.none, Command.no_exec);
fun update_entry id exec =
map_entries (Entries.update (id, exec));
@@ -234,10 +201,20 @@
(** main state -- document structure and execution process **)
+type execution =
+ {version_id: Document_ID.version,
+ group: Future.group,
+ running: bool Unsynchronized.ref};
+
+val no_execution =
+ {version_id = Document_ID.none,
+ group = Future.new_group NONE,
+ running = Unsynchronized.ref false};
+
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*)
+ {versions: version Inttab.table, (*version id -> document content*)
+ commands: (string * Token.T list lazy) Inttab.table, (*command id -> named span*)
+ execution: execution} (*current execution process*)
with
fun make_state (versions, commands, execution) =
@@ -247,98 +224,85 @@
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, no_execution);
fun execution_of (State {execution, ...}) = execution;
(* document versions *)
-fun define_version (id: version_id) version =
+fun define_version version_id version =
map_state (fn (versions, commands, _) =>
let
- val versions' = Inttab.update_new (id, version) versions
+ val versions' = Inttab.update_new (version_id, version) versions
handle Inttab.DUP dup => err_dup "document version" dup;
- val execution' = (id, Future.new_group NONE, Unsynchronized.ref true);
+ val execution' =
+ {version_id = version_id,
+ group = Future.new_group NONE,
+ running = Unsynchronized.ref true};
in (versions', commands, execution') end);
-fun the_version (State {versions, ...}) (id: version_id) =
- (case Inttab.lookup versions id of
- NONE => err_undef "document version" id
+fun the_version (State {versions, ...}) version_id =
+ (case Inttab.lookup versions version_id of
+ NONE => err_undef "document version" version_id
| SOME version => version);
-fun delete_version (id: version_id) versions = Inttab.delete id versions
- handle Inttab.UNDEF _ => err_undef "document version" id;
+fun delete_version version_id versions =
+ Inttab.delete version_id versions
+ handle Inttab.UNDEF _ => err_undef "document version" version_id;
(* commands *)
-fun define_command (id: command_id) name text =
+fun define_command command_id name text =
map_state (fn (versions, commands, execution) =>
let
- val id_string = print_id 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)
- ());
+ val id = Document_ID.print command_id;
+ val span =
+ Lazy.lazy (fn () =>
+ Position.setmp_thread_data (Position.id_only id)
+ (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ());
val _ =
- Position.setmp_thread_data (Position.id_only id_string)
+ Position.setmp_thread_data (Position.id_only id)
(fn () => Output.status (Markup.markup_only Markup.accepted)) ();
val commands' =
- Inttab.update_new (id, (name, span)) commands
+ Inttab.update_new (command_id, (name, span)) commands
handle Inttab.DUP dup => err_dup "command" dup;
in (versions, commands', execution) end);
-fun the_command (State {commands, ...}) (id: command_id) =
- (case Inttab.lookup commands id of
- NONE => err_undef "command" id
+fun the_command (State {commands, ...}) command_id =
+ (case Inttab.lookup commands command_id of
+ NONE => err_undef "command" command_id
| SOME command => command);
end;
-fun remove_versions ids state = state |> map_state (fn (versions, _, execution) =>
+fun remove_versions version_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));
+ val _ =
+ member (op =) version_ids (#version_id execution) andalso
+ error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution));
- val versions' = fold delete_version ids versions;
+ val versions' = fold delete_version version_ids versions;
val commands' =
(versions', Inttab.empty) |->
Inttab.fold (fn (_, version) => nodes_of version |>
String_Graph.fold (fn (_, (node, _)) => node |>
- iterate_entries (fn ((_, id), _) =>
- SOME o Inttab.insert (K true) (id, the_command state id))));
+ iterate_entries (fn ((_, command_id), _) =>
+ SOME o Inttab.insert (K true) (command_id, the_command state command_id))));
in (versions', commands', execution) end);
-(* consolidated states *)
-
-fun stable_goals exec_id =
- not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
-
-fun stable_eval ((exec_id, (eval, _)): exec) =
- stable_goals exec_id andalso Command.memo_stable eval;
-
-fun stable_print ({exec_id, print, ...}: Command.print) =
- stable_goals exec_id andalso Command.memo_stable print;
-
-fun finished_theory node =
- (case Exn.capture (Command.memo_result o the) (get_result node) of
- Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
- | _ => false);
-
-
(** document execution **)
-val discontinue_execution = execution_of #> (fn (_, _, running) => running := false);
-val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group);
-val terminate_execution = execution_of #> (fn (_, group, _) => Future.terminate group);
+val discontinue_execution = execution_of #> (fn {running, ...} => running := false);
+val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group);
+val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group);
fun start_execution state =
let
- val (version_id, group, running) = execution_of state;
+ val {version_id, group, running} = execution_of state;
val _ =
(singleton o Future.forks)
{name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
@@ -355,7 +319,7 @@
(fn () =>
iterate_entries (fn (_, opt_exec) => fn () =>
(case opt_exec of
- SOME exec => if ! running then SOME (exec_run exec) else NONE
+ SOME exec => if ! running then SOME (Command.execute exec) else NONE
| NONE => NONE)) node ()))));
in () end;
@@ -396,10 +360,9 @@
SOME thy => thy
| NONE =>
Toplevel.end_theory (Position.file_only import)
- (#state
- (Command.memo_result
- (the_default Command.no_eval
- (get_result (snd (the (AList.lookup (op =) deps import)))))))));
+ (case get_result (snd (the (AList.lookup (op =) deps import))) of
+ NONE => Toplevel.toplevel
+ | SOME eval => Command.eval_result_state eval)));
val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
in Thy_Load.begin_theory master_dir header parents end;
@@ -424,10 +387,11 @@
val same' =
(case opt_exec of
NONE => false
- | SOME (exec_id, exec) =>
+ | SOME (eval, _) =>
(case lookup_entry node0 id of
NONE => false
- | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_eval (exec_id, exec)));
+ | SOME (eval0, _) =>
+ #exec_id eval = #exec_id eval0 andalso Command.stable_eval eval));
in SOME (same', (prev, flags')) end
else NONE;
val (same, (common, flags)) =
@@ -439,56 +403,42 @@
else (common, flags)
end;
+fun illegal_init _ = error "Illegal theory header after end of theory";
+
fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) =
if not proper_init andalso is_none init then NONE
else
let
+ val (_, (eval, _)) = command_exec;
val (command_name, span) = the_command state command_id' ||> Lazy.force;
-
- fun illegal_init _ = error "Illegal theory header after end of theory";
- val (modify_init, init') =
- if Keyword.is_theory_begin command_name then
- (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
- else (I, init);
-
- val exec_id' = new_id ();
- 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'))
- (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 command_exec' = (command_id', (exec_id', (eval', prints')));
+ val init' = if Keyword.is_theory_begin command_name then NONE else init;
+ val eval' = Command.eval (fn () => the_default illegal_init init span) span eval;
+ val prints' = if command_visible then Command.print command_name eval' else [];
+ val command_exec' = (command_id', (eval', prints'));
in SOME (command_exec' :: execs, command_exec', init') end;
fun update_prints state node command_id =
(case the_entry node command_id of
- SOME (exec_id, (eval, prints)) =>
+ SOME (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
- SOME print => if stable_print print then print else new_print
+ SOME print => if Command.stable_print print then print else new_print
| NONE => new_print));
in
if eq_list (op = o pairself #exec_id) (prints, prints') then NONE
- else SOME (command_id, (exec_id, (eval, prints')))
+ else SOME (command_id, (eval, prints'))
end
| NONE => NONE);
in
-fun update (old_id: version_id) (new_id: version_id) edits state =
+fun update old_version_id new_version_id edits state =
let
- val old_version = the_version state old_id;
+ val old_version = the_version state old_version_id;
val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
val nodes = nodes_of new_version;
@@ -526,7 +476,7 @@
else last_common state last_visible node0 node;
val common_command_exec = the_default_entry node common;
- val (new_execs, (command_id', (_, (eval', _))), _) =
+ val (new_execs, (command_id', (eval', _)), _) =
([], common_command_exec, if initial then SOME init else NONE) |>
(still_visible orelse node_required) ?
iterate_entries_after common
@@ -536,18 +486,19 @@
val updated_execs =
(visible_commands, new_execs) |-> Inttab.fold (fn (id, ()) =>
- if exists (fn (_, (id', _)) => id = id') new_execs then I
+ if exists (fn (_, ({exec_id = id', ...}, _)) => id = id') new_execs then I
else append (the_list (update_prints state node id)));
val no_execs =
iterate_entries_after common
(fn ((_, id0), exec0) => fn res =>
if is_none exec0 then NONE
- else if exists (fn (_, (id, _)) => id0 = id) updated_execs
+ else if exists (fn (_, ({exec_id = id, ...}, _)) => id0 = id) updated_execs
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';
@@ -568,11 +519,11 @@
val command_execs =
map (rpair []) (maps #1 updated) @
- map (fn (command_id, exec) => (command_id, exec_ids_of exec)) (maps #2 updated);
+ map (fn (command_id, exec) => (command_id, Command.exec_ids exec)) (maps #2 updated);
val updated_nodes = map_filter #3 updated;
val state' = state
- |> define_version new_id (fold put_node updated_nodes new_version);
+ |> define_version new_version_id (fold put_node updated_nodes new_version);
in (command_execs, state') end;
end;
--- a/src/Pure/PIDE/document.scala Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/document.scala Fri Jul 05 23:17:39 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.Generic): 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.Generic, 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 23:17:39 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 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 generic = int;
+type version = generic;
+type command = generic;
+type exec = generic;
+
+val none = 0;
+val make = Counter.make ();
+
+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 23:17:39 2013 +0200
@@ -0,0 +1,25 @@
+/* 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 Generic = Long
+ type Version = Generic
+ type Command = Generic
+ type Exec = Generic
+
+ val none: Generic = 0
+ val make = Counter.make()
+
+ 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.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Jul 05 23:17:39 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 16:45:31 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Fri Jul 05 23:17:39 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.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, 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, 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, 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(command.id), encode(command.name), encode(command.source))
+ Document_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(old_id), Document_ID(new_id), edits_yxml)
}
def remove_versions(versions: List[Document.Version])
--- a/src/Pure/ROOT Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/ROOT Fri Jul 05 23:17:39 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 16:45:31 2013 +0200
+++ b/src/Pure/ROOT.ML Fri Jul 05 23:17:39 2013 +0200
@@ -22,6 +22,7 @@
use "Concurrent/synchronized.ML";
if Multithreading.available then ()
else use "Concurrent/synchronized_sequential.ML";
+use "Concurrent/counter.ML";
use "General/properties.ML";
use "General/output.ML";
@@ -256,6 +257,7 @@
(*toplevel transactions*)
use "Isar/proof_node.ML";
+use "PIDE/document_id.ML";
use "Isar/toplevel.ML";
(*theory documents*)
--- a/src/Pure/System/invoke_scala.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/System/invoke_scala.ML Fri Jul 05 23:17:39 2013 +0200
@@ -19,7 +19,7 @@
(* pending promises *)
-val new_id = string_of_int o Synchronized.counter ();
+val new_id = string_of_int o Counter.make ();
val promises =
Synchronized.var "Invoke_Scala.promises" (Symtab.empty: string future Symtab.table);
--- a/src/Pure/System/session.scala Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/System/session.scala Fri Jul 05 23:17:39 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.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, 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, 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/Pure/System/system_channel.scala Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/System/system_channel.scala Fri Jul 05 23:17:39 2013 +0200
@@ -31,7 +31,7 @@
private object Fifo_Channel
{
- private val next_fifo = Counter()
+ private val next_fifo = Counter.make()
}
private class Fifo_Channel extends System_Channel
--- a/src/Pure/Thy/thy_load.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Thy/thy_load.ML Fri Jul 05 23:17:39 2013 +0200
@@ -217,8 +217,7 @@
let
fun prepare_span span =
Thy_Syntax.span_content span
- |> Command.read
- |> Toplevel.modify_init init
+ |> Command.read init
|> (fn tr => Toplevel.put_timing (last_timing tr) tr);
fun element_result span_elem (st, _) =
--- a/src/Pure/Thy/thy_syntax.scala Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Fri Jul 05 23:17:39 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()
}
}
@@ -77,9 +77,9 @@
/** parse spans **/
- def parse_spans(toks: List[Token]): List[Command.Span] =
+ def parse_spans(toks: List[Token]): List[List[Token]] =
{
- val result = new mutable.ListBuffer[Command.Span]
+ val result = new mutable.ListBuffer[List[Token]]
val span = new mutable.ListBuffer[Token]
def flush() { if (!span.isEmpty) { result += span.toList; span.clear } }
@@ -198,7 +198,7 @@
/* reparse range of command spans */
@tailrec private def chop_common(
- cmds: List[Command], spans: List[Command.Span]): (List[Command], List[Command.Span]) =
+ cmds: List[Command], spans: List[List[Token]]): (List[Command], List[List[Token]]) =
(cmds, spans) match {
case (c :: cs, s :: ss) if c.span == s => chop_common(cs, ss)
case _ => (cmds, spans)
@@ -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/Tools/proof_general.ML Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML Fri Jul 05 23:17:39 2013 +0200
@@ -152,7 +152,7 @@
| opt_attr name (SOME value) = attr name value;
val pgip_id = "dummy";
-val pgip_serial = Synchronized.counter ();
+val pgip_serial = Counter.make ();
fun output_pgip refid refseq content =
XML.Elem (("pgip",
--- a/src/Pure/build-jars Fri Jul 05 16:45:31 2013 +0200
+++ b/src/Pure/build-jars Fri Jul 05 23:17:39 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 16:45:31 2013 +0200
+++ b/src/Tools/jEdit/src/active.scala Fri Jul 05 23:17:39 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.Exec, 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 16:45:31 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Jul 05 23:17:39 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 16:45:31 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Fri Jul 05 23:17:39 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