--- a/src/Pure/General/markup.ML Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Pure/General/markup.ML Fri Sep 02 16:58:00 2011 -0700
@@ -107,8 +107,6 @@
val joinedN: string val joined: T
val failedN: string val failed: T
val finishedN: string val finished: T
- val versionN: string
- val assignN: string val assign: int -> T
val serialN: string
val legacyN: string val legacy: T
val promptN: string val prompt: T
@@ -117,6 +115,7 @@
val no_reportN: string val no_report: T
val badN: string val bad: T
val functionN: string
+ val assign_execs: Properties.T
val invoke_scala: string -> string -> Properties.T
val cancel_scala: string -> Properties.T
val no_output: Output.output * Output.output
@@ -349,12 +348,6 @@
val (finishedN, finished) = markup_elem "finished";
-(* interactive documents *)
-
-val versionN = "version";
-val (assignN, assign) = markup_int "assign" versionN;
-
-
(* messages *)
val serialN = "serial";
@@ -373,6 +366,8 @@
val functionN = "function"
+val assign_execs = [(functionN, "assign_execs")];
+
fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
--- a/src/Pure/General/markup.scala Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Pure/General/markup.scala Fri Sep 02 16:58:00 2011 -0700
@@ -273,6 +273,8 @@
val FUNCTION = "function"
val Function = new Properties.String(FUNCTION)
+ val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
+
val INVOKE_SCALA = "invoke_scala"
object Invoke_Scala
{
--- a/src/Pure/Isar/outer_syntax.ML Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Pure/Isar/outer_syntax.ML Fri Sep 02 16:58:00 2011 -0700
@@ -34,10 +34,9 @@
val process_file: Path.T -> theory -> theory
type isar
val isar: TextIO.instream -> bool -> isar
- val read_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
+ val read_command: Position.T -> string -> Toplevel.transition
val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
(Toplevel.transition * Toplevel.transition list) list
- val read_command: Position.T -> string -> Toplevel.transition
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -255,38 +254,37 @@
val not_singleton = "Exactly one command expected";
-fun read_span outer_syntax span =
+fun read_span outer_syntax toks =
let
val commands = lookup_commands outer_syntax;
- val range_pos = Position.set_range (Thy_Syntax.span_range span);
- val toks = Thy_Syntax.span_content span;
+ val range_pos = Position.set_range (Token.range toks);
val _ = List.app Thy_Syntax.report_token toks;
in
(case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
[tr] =>
if Keyword.is_control (Toplevel.name_of tr) then
- (Toplevel.malformed range_pos "Illegal control command", true)
+ (Toplevel.malformed (Toplevel.pos_of tr) "Illegal control command", true)
else (tr, true)
| [] => (Toplevel.ignored range_pos, false)
| _ => (Toplevel.malformed range_pos not_singleton, true))
handle ERROR msg => (Toplevel.malformed range_pos msg, true)
end;
+fun read_command pos str =
+ let
+ val (lexs, outer_syntax) = get_syntax ();
+ val toks = Thy_Syntax.parse_tokens lexs pos str;
+ in #1 (read_span outer_syntax toks) end;
+
fun read_element outer_syntax init {head, proof, proper_proof} =
let
- val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
- val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
+ val read = read_span outer_syntax o Thy_Syntax.span_content;
+ val (tr, proper_head) = read head |>> Toplevel.modify_init init;
+ val proof_trs = map read proof |> filter #2 |> map #1;
in
if proper_head andalso proper_proof then [(tr, proof_trs)]
else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
end;
-fun read_command pos str =
- let val (lexs, outer_syntax) = get_syntax () in
- (case Thy_Syntax.parse_spans lexs pos str of
- [span] => #1 (read_span outer_syntax span)
- | _ => Toplevel.malformed pos not_singleton)
- end;
-
end;
--- a/src/Pure/Isar/token.ML Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Pure/Isar/token.ML Fri Sep 02 16:58:00 2011 -0700
@@ -18,6 +18,7 @@
val position_of: T -> Position.T
val end_position_of: T -> Position.T
val pos_of: T -> string
+ val range: T list -> Position.range
val eof: T
val is_eof: T -> bool
val not_eof: T -> bool
@@ -122,6 +123,13 @@
val pos_of = Position.str_of o position_of;
+fun range [] = (Position.none, Position.none)
+ | range toks =
+ let
+ val start_pos = position_of (hd toks);
+ val end_pos = end_position_of (List.last toks);
+ in (start_pos, end_pos) end;
+
(* control tokens *)
--- a/src/Pure/PIDE/document.ML Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Pure/PIDE/document.ML Fri Sep 02 16:58:00 2011 -0700
@@ -25,7 +25,6 @@
type state
val init_state: state
val define_command: command_id -> string -> string -> state -> state
- val join_commands: state -> state
val cancel_execution: state -> Future.task list
val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
val update: version_id -> version_id -> edit list -> state ->
@@ -237,9 +236,7 @@
abstype state = State of
{versions: version Inttab.table, (*version_id -> document content*)
- commands:
- (string * Toplevel.transition future) Inttab.table * (*command_id -> name * transition*)
- Toplevel.transition future list, (*recent commands to be joined*)
+ commands: (string * Toplevel.transition future) Inttab.table, (*command_id -> name * transition*)
execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
(*exec_id -> command_id with eval/print process*)
execution: Future.group} (*global execution process*)
@@ -253,7 +250,7 @@
val init_state =
make_state (Inttab.make [(no_id, empty_version)],
- (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []),
+ Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))],
Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
Future.new_group NONE);
@@ -275,27 +272,26 @@
(* commands *)
fun define_command (id: command_id) name text =
- map_state (fn (versions, (commands, recent), execs, execution) =>
+ map_state (fn (versions, commands, execs, execution) =>
let
val id_string = print_id id;
- val tr =
- Future.fork_pri 2 (fn () =>
- Position.setmp_thread_data (Position.id_only id_string)
- (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
+ val future =
+ (singleton o Future.forks)
+ {name = "Document.define_command", group = SOME (Future.new_group NONE),
+ deps = [], pri = ~1, interrupts = false}
+ (fn () =>
+ Position.setmp_thread_data (Position.id_only id_string)
+ (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
val commands' =
- Inttab.update_new (id, (name, tr)) commands
+ Inttab.update_new (id, (name, future)) commands
handle Inttab.DUP dup => err_dup "command" dup;
- in (versions, (commands', tr :: recent), execs, execution) end);
+ in (versions, commands', execs, execution) end);
fun the_command (State {commands, ...}) (id: command_id) =
- (case Inttab.lookup (#1 commands) id of
+ (case Inttab.lookup commands id of
NONE => err_undef "command" id
| SOME command => command);
-val join_commands =
- map_state (fn (versions, (commands, recent), execs, execution) =>
- (Future.join_results recent; (versions, (commands, []), execs, execution)));
-
(* command executions *)
@@ -419,20 +415,16 @@
if bad_init andalso is_none init then NONE
else
let
- val (name, tr0) = the_command state command_id';
+ val (name, tr0) = the_command state command_id' ||> Future.join;
val (modify_init, init') =
if Keyword.is_theory_begin name then
(Toplevel.modify_init (the_default illegal_init init), NONE)
else (I, init);
- val exec_id' = new_id ();
- val exec' =
- snd exec |> Lazy.map (fn (st, _) =>
- let val tr =
- Future.join tr0
- |> modify_init
- |> Toplevel.put_id (print_id exec_id');
- in run_command tr st end)
- |> pair command_id';
+ val exec_id' = new_id ();
+ val tr = tr0
+ |> modify_init
+ |> Toplevel.put_id (print_id exec_id');
+ val exec' = (command_id', Lazy.map (fn (st, _) => run_command tr st) (snd exec));
in SOME ((exec_id', exec') :: execs, exec', init') end;
fun make_required nodes =
--- a/src/Pure/PIDE/isar_document.ML Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Pure/PIDE/isar_document.ML Fri Sep 02 16:58:00 2011 -0700
@@ -55,15 +55,14 @@
val running = Document.cancel_execution state;
val (assignment, state1) = Document.update old_id new_id edits state;
val _ = Future.join_tasks running;
- val state2 = Document.join_commands state1;
val _ =
- Output.status (Markup.markup (Markup.assign new_id)
- (assignment |>
+ Output.raw_message Markup.assign_execs
+ ((new_id, assignment) |>
let open XML.Encode
- in pair (list (pair int (option int))) (list (pair string (option int))) end
- |> YXML.string_of_body));
- val state3 = Document.execute new_id state2;
- in state3 end));
+ in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
+ |> YXML.string_of_body);
+ val state2 = Document.execute new_id state1;
+ in state2 end));
val _ =
Isabelle_Process.add_command "Isar_Document.invoke_scala"
--- a/src/Pure/PIDE/isar_document.scala Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Pure/PIDE/isar_document.scala Fri Sep 02 16:58:00 2011 -0700
@@ -13,19 +13,16 @@
object Assign
{
- def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
- msg match {
- case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
- try {
- import XML.Decode._
- val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body)
- Some(id, a)
- }
- catch {
- case _: XML.XML_Atom => None
- case _: XML.XML_Body => None
- }
- case _ => None
+ def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
+ try {
+ import XML.Decode._
+ val body = YXML.parse_body(text)
+ Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
+ }
+ catch {
+ case ERROR(_) => None
+ case _: XML.XML_Atom => None
+ case _: XML.XML_Body => None
}
}
--- a/src/Pure/System/session.scala Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Pure/System/session.scala Fri Sep 02 16:58:00 2011 -0700
@@ -288,6 +288,13 @@
catch {
case _: Document.State.Fail => bad_result(result)
}
+ case Markup.Assign_Execs if result.is_raw =>
+ XML.content(result.body).mkString match {
+ case Isar_Document.Assign(id, assign) =>
+ try { handle_assign(id, assign) }
+ catch { case _: Document.State.Fail => bad_result(result) }
+ case _ => bad_result(result)
+ }
case Markup.Invoke_Scala(name, id) if result.is_raw =>
Future.fork {
val arg = XML.content(result.body).mkString
@@ -311,9 +318,6 @@
else if (result.is_stdout) { }
else if (result.is_status) {
result.body match {
- case List(Isar_Document.Assign(id, assign)) =>
- try { handle_assign(id, assign) }
- catch { case _: Document.State.Fail => bad_result(result) }
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
--- a/src/Pure/Thy/thy_syntax.ML Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.ML Fri Sep 02 16:58:00 2011 -0700
@@ -16,7 +16,6 @@
type span
val span_kind: span -> span_kind
val span_content: span -> Token.T list
- val span_range: span -> Position.range
val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
val present_span: span -> Output.output
@@ -101,15 +100,6 @@
fun span_kind (Span (k, _)) = k;
fun span_content (Span (_, toks)) = toks;
-fun span_range span =
- (case span_content span of
- [] => (Position.none, Position.none)
- | toks =>
- let
- val start_pos = Token.position_of (hd toks);
- val end_pos = Token.end_position_of (List.last toks);
- in (start_pos, end_pos) end);
-
(* parse *)
--- a/src/Tools/jEdit/src/text_area_painter.scala Fri Sep 02 16:57:51 2011 -0700
+++ b/src/Tools/jEdit/src/text_area_painter.scala Fri Sep 02 16:58:00 2011 -0700
@@ -201,6 +201,7 @@
x + w < clip_rect.x + clip_rect.width && chunk.accessable)
{
val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
+ val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
val chunk_font = chunk.style.getFont
val chunk_color = chunk.style.getForegroundColor
@@ -229,7 +230,7 @@
var x1 = x + w
gfx.setFont(chunk_font)
for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
- val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
+ val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
gfx.setColor(info.getOrElse(chunk_color))
range.try_restrict(caret_range) match {