1.1 --- a/src/Pure/General/markup.ML Fri Sep 02 16:57:51 2011 -0700
1.2 +++ b/src/Pure/General/markup.ML Fri Sep 02 16:58:00 2011 -0700
1.3 @@ -107,8 +107,6 @@
1.4 val joinedN: string val joined: T
1.5 val failedN: string val failed: T
1.6 val finishedN: string val finished: T
1.7 - val versionN: string
1.8 - val assignN: string val assign: int -> T
1.9 val serialN: string
1.10 val legacyN: string val legacy: T
1.11 val promptN: string val prompt: T
1.12 @@ -117,6 +115,7 @@
1.13 val no_reportN: string val no_report: T
1.14 val badN: string val bad: T
1.15 val functionN: string
1.16 + val assign_execs: Properties.T
1.17 val invoke_scala: string -> string -> Properties.T
1.18 val cancel_scala: string -> Properties.T
1.19 val no_output: Output.output * Output.output
1.20 @@ -349,12 +348,6 @@
1.21 val (finishedN, finished) = markup_elem "finished";
1.22
1.23
1.24 -(* interactive documents *)
1.25 -
1.26 -val versionN = "version";
1.27 -val (assignN, assign) = markup_int "assign" versionN;
1.28 -
1.29 -
1.30 (* messages *)
1.31
1.32 val serialN = "serial";
1.33 @@ -373,6 +366,8 @@
1.34
1.35 val functionN = "function"
1.36
1.37 +val assign_execs = [(functionN, "assign_execs")];
1.38 +
1.39 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)];
1.40 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)];
1.41
2.1 --- a/src/Pure/General/markup.scala Fri Sep 02 16:57:51 2011 -0700
2.2 +++ b/src/Pure/General/markup.scala Fri Sep 02 16:58:00 2011 -0700
2.3 @@ -273,6 +273,8 @@
2.4 val FUNCTION = "function"
2.5 val Function = new Properties.String(FUNCTION)
2.6
2.7 + val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
2.8 +
2.9 val INVOKE_SCALA = "invoke_scala"
2.10 object Invoke_Scala
2.11 {
3.1 --- a/src/Pure/Isar/outer_syntax.ML Fri Sep 02 16:57:51 2011 -0700
3.2 +++ b/src/Pure/Isar/outer_syntax.ML Fri Sep 02 16:58:00 2011 -0700
3.3 @@ -34,10 +34,9 @@
3.4 val process_file: Path.T -> theory -> theory
3.5 type isar
3.6 val isar: TextIO.instream -> bool -> isar
3.7 - val read_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
3.8 + val read_command: Position.T -> string -> Toplevel.transition
3.9 val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
3.10 (Toplevel.transition * Toplevel.transition list) list
3.11 - val read_command: Position.T -> string -> Toplevel.transition
3.12 end;
3.13
3.14 structure Outer_Syntax: OUTER_SYNTAX =
3.15 @@ -255,38 +254,37 @@
3.16
3.17 val not_singleton = "Exactly one command expected";
3.18
3.19 -fun read_span outer_syntax span =
3.20 +fun read_span outer_syntax toks =
3.21 let
3.22 val commands = lookup_commands outer_syntax;
3.23 - val range_pos = Position.set_range (Thy_Syntax.span_range span);
3.24 - val toks = Thy_Syntax.span_content span;
3.25 + val range_pos = Position.set_range (Token.range toks);
3.26 val _ = List.app Thy_Syntax.report_token toks;
3.27 in
3.28 (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
3.29 [tr] =>
3.30 if Keyword.is_control (Toplevel.name_of tr) then
3.31 - (Toplevel.malformed range_pos "Illegal control command", true)
3.32 + (Toplevel.malformed (Toplevel.pos_of tr) "Illegal control command", true)
3.33 else (tr, true)
3.34 | [] => (Toplevel.ignored range_pos, false)
3.35 | _ => (Toplevel.malformed range_pos not_singleton, true))
3.36 handle ERROR msg => (Toplevel.malformed range_pos msg, true)
3.37 end;
3.38
3.39 +fun read_command pos str =
3.40 + let
3.41 + val (lexs, outer_syntax) = get_syntax ();
3.42 + val toks = Thy_Syntax.parse_tokens lexs pos str;
3.43 + in #1 (read_span outer_syntax toks) end;
3.44 +
3.45 fun read_element outer_syntax init {head, proof, proper_proof} =
3.46 let
3.47 - val (tr, proper_head) = read_span outer_syntax head |>> Toplevel.modify_init init;
3.48 - val proof_trs = map (read_span outer_syntax) proof |> filter #2 |> map #1;
3.49 + val read = read_span outer_syntax o Thy_Syntax.span_content;
3.50 + val (tr, proper_head) = read head |>> Toplevel.modify_init init;
3.51 + val proof_trs = map read proof |> filter #2 |> map #1;
3.52 in
3.53 if proper_head andalso proper_proof then [(tr, proof_trs)]
3.54 else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
3.55 end;
3.56
3.57 -fun read_command pos str =
3.58 - let val (lexs, outer_syntax) = get_syntax () in
3.59 - (case Thy_Syntax.parse_spans lexs pos str of
3.60 - [span] => #1 (read_span outer_syntax span)
3.61 - | _ => Toplevel.malformed pos not_singleton)
3.62 - end;
3.63 -
3.64 end;
3.65
4.1 --- a/src/Pure/Isar/token.ML Fri Sep 02 16:57:51 2011 -0700
4.2 +++ b/src/Pure/Isar/token.ML Fri Sep 02 16:58:00 2011 -0700
4.3 @@ -18,6 +18,7 @@
4.4 val position_of: T -> Position.T
4.5 val end_position_of: T -> Position.T
4.6 val pos_of: T -> string
4.7 + val range: T list -> Position.range
4.8 val eof: T
4.9 val is_eof: T -> bool
4.10 val not_eof: T -> bool
4.11 @@ -122,6 +123,13 @@
4.12
4.13 val pos_of = Position.str_of o position_of;
4.14
4.15 +fun range [] = (Position.none, Position.none)
4.16 + | range toks =
4.17 + let
4.18 + val start_pos = position_of (hd toks);
4.19 + val end_pos = end_position_of (List.last toks);
4.20 + in (start_pos, end_pos) end;
4.21 +
4.22
4.23 (* control tokens *)
4.24
5.1 --- a/src/Pure/PIDE/document.ML Fri Sep 02 16:57:51 2011 -0700
5.2 +++ b/src/Pure/PIDE/document.ML Fri Sep 02 16:58:00 2011 -0700
5.3 @@ -25,7 +25,6 @@
5.4 type state
5.5 val init_state: state
5.6 val define_command: command_id -> string -> string -> state -> state
5.7 - val join_commands: state -> state
5.8 val cancel_execution: state -> Future.task list
5.9 val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
5.10 val update: version_id -> version_id -> edit list -> state ->
5.11 @@ -237,9 +236,7 @@
5.12
5.13 abstype state = State of
5.14 {versions: version Inttab.table, (*version_id -> document content*)
5.15 - commands:
5.16 - (string * Toplevel.transition future) Inttab.table * (*command_id -> name * transition*)
5.17 - Toplevel.transition future list, (*recent commands to be joined*)
5.18 + commands: (string * Toplevel.transition future) Inttab.table, (*command_id -> name * transition*)
5.19 execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
5.20 (*exec_id -> command_id with eval/print process*)
5.21 execution: Future.group} (*global execution process*)
5.22 @@ -253,7 +250,7 @@
5.23
5.24 val init_state =
5.25 make_state (Inttab.make [(no_id, empty_version)],
5.26 - (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []),
5.27 + Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))],
5.28 Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
5.29 Future.new_group NONE);
5.30
5.31 @@ -275,27 +272,26 @@
5.32 (* commands *)
5.33
5.34 fun define_command (id: command_id) name text =
5.35 - map_state (fn (versions, (commands, recent), execs, execution) =>
5.36 + map_state (fn (versions, commands, execs, execution) =>
5.37 let
5.38 val id_string = print_id id;
5.39 - val tr =
5.40 - Future.fork_pri 2 (fn () =>
5.41 - Position.setmp_thread_data (Position.id_only id_string)
5.42 - (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
5.43 + val future =
5.44 + (singleton o Future.forks)
5.45 + {name = "Document.define_command", group = SOME (Future.new_group NONE),
5.46 + deps = [], pri = ~1, interrupts = false}
5.47 + (fn () =>
5.48 + Position.setmp_thread_data (Position.id_only id_string)
5.49 + (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
5.50 val commands' =
5.51 - Inttab.update_new (id, (name, tr)) commands
5.52 + Inttab.update_new (id, (name, future)) commands
5.53 handle Inttab.DUP dup => err_dup "command" dup;
5.54 - in (versions, (commands', tr :: recent), execs, execution) end);
5.55 + in (versions, commands', execs, execution) end);
5.56
5.57 fun the_command (State {commands, ...}) (id: command_id) =
5.58 - (case Inttab.lookup (#1 commands) id of
5.59 + (case Inttab.lookup commands id of
5.60 NONE => err_undef "command" id
5.61 | SOME command => command);
5.62
5.63 -val join_commands =
5.64 - map_state (fn (versions, (commands, recent), execs, execution) =>
5.65 - (Future.join_results recent; (versions, (commands, []), execs, execution)));
5.66 -
5.67
5.68 (* command executions *)
5.69
5.70 @@ -419,20 +415,16 @@
5.71 if bad_init andalso is_none init then NONE
5.72 else
5.73 let
5.74 - val (name, tr0) = the_command state command_id';
5.75 + val (name, tr0) = the_command state command_id' ||> Future.join;
5.76 val (modify_init, init') =
5.77 if Keyword.is_theory_begin name then
5.78 (Toplevel.modify_init (the_default illegal_init init), NONE)
5.79 else (I, init);
5.80 - val exec_id' = new_id ();
5.81 - val exec' =
5.82 - snd exec |> Lazy.map (fn (st, _) =>
5.83 - let val tr =
5.84 - Future.join tr0
5.85 - |> modify_init
5.86 - |> Toplevel.put_id (print_id exec_id');
5.87 - in run_command tr st end)
5.88 - |> pair command_id';
5.89 + val exec_id' = new_id ();
5.90 + val tr = tr0
5.91 + |> modify_init
5.92 + |> Toplevel.put_id (print_id exec_id');
5.93 + val exec' = (command_id', Lazy.map (fn (st, _) => run_command tr st) (snd exec));
5.94 in SOME ((exec_id', exec') :: execs, exec', init') end;
5.95
5.96 fun make_required nodes =
6.1 --- a/src/Pure/PIDE/isar_document.ML Fri Sep 02 16:57:51 2011 -0700
6.2 +++ b/src/Pure/PIDE/isar_document.ML Fri Sep 02 16:58:00 2011 -0700
6.3 @@ -55,15 +55,14 @@
6.4 val running = Document.cancel_execution state;
6.5 val (assignment, state1) = Document.update old_id new_id edits state;
6.6 val _ = Future.join_tasks running;
6.7 - val state2 = Document.join_commands state1;
6.8 val _ =
6.9 - Output.status (Markup.markup (Markup.assign new_id)
6.10 - (assignment |>
6.11 + Output.raw_message Markup.assign_execs
6.12 + ((new_id, assignment) |>
6.13 let open XML.Encode
6.14 - in pair (list (pair int (option int))) (list (pair string (option int))) end
6.15 - |> YXML.string_of_body));
6.16 - val state3 = Document.execute new_id state2;
6.17 - in state3 end));
6.18 + in pair int (pair (list (pair int (option int))) (list (pair string (option int)))) end
6.19 + |> YXML.string_of_body);
6.20 + val state2 = Document.execute new_id state1;
6.21 + in state2 end));
6.22
6.23 val _ =
6.24 Isabelle_Process.add_command "Isar_Document.invoke_scala"
7.1 --- a/src/Pure/PIDE/isar_document.scala Fri Sep 02 16:57:51 2011 -0700
7.2 +++ b/src/Pure/PIDE/isar_document.scala Fri Sep 02 16:58:00 2011 -0700
7.3 @@ -13,19 +13,16 @@
7.4
7.5 object Assign
7.6 {
7.7 - def unapply(msg: XML.Tree): Option[(Document.Version_ID, Document.Assign)] =
7.8 - msg match {
7.9 - case XML.Elem(Markup(Markup.ASSIGN, List((Markup.VERSION, Document.ID(id)))), body) =>
7.10 - try {
7.11 - import XML.Decode._
7.12 - val a = pair(list(pair(long, option(long))), list(pair(string, option(long))))(body)
7.13 - Some(id, a)
7.14 - }
7.15 - catch {
7.16 - case _: XML.XML_Atom => None
7.17 - case _: XML.XML_Body => None
7.18 - }
7.19 - case _ => None
7.20 + def unapply(text: String): Option[(Document.Version_ID, Document.Assign)] =
7.21 + try {
7.22 + import XML.Decode._
7.23 + val body = YXML.parse_body(text)
7.24 + Some(pair(long, pair(list(pair(long, option(long))), list(pair(string, option(long)))))(body))
7.25 + }
7.26 + catch {
7.27 + case ERROR(_) => None
7.28 + case _: XML.XML_Atom => None
7.29 + case _: XML.XML_Body => None
7.30 }
7.31 }
7.32
8.1 --- a/src/Pure/System/session.scala Fri Sep 02 16:57:51 2011 -0700
8.2 +++ b/src/Pure/System/session.scala Fri Sep 02 16:58:00 2011 -0700
8.3 @@ -288,6 +288,13 @@
8.4 catch {
8.5 case _: Document.State.Fail => bad_result(result)
8.6 }
8.7 + case Markup.Assign_Execs if result.is_raw =>
8.8 + XML.content(result.body).mkString match {
8.9 + case Isar_Document.Assign(id, assign) =>
8.10 + try { handle_assign(id, assign) }
8.11 + catch { case _: Document.State.Fail => bad_result(result) }
8.12 + case _ => bad_result(result)
8.13 + }
8.14 case Markup.Invoke_Scala(name, id) if result.is_raw =>
8.15 Future.fork {
8.16 val arg = XML.content(result.body).mkString
8.17 @@ -311,9 +318,6 @@
8.18 else if (result.is_stdout) { }
8.19 else if (result.is_status) {
8.20 result.body match {
8.21 - case List(Isar_Document.Assign(id, assign)) =>
8.22 - try { handle_assign(id, assign) }
8.23 - catch { case _: Document.State.Fail => bad_result(result) }
8.24 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
8.25 case List(Keyword.Keyword_Decl(name)) => syntax += name
8.26 case List(Thy_Info.Loaded_Theory(name)) => thy_load.register_thy(name)
9.1 --- a/src/Pure/Thy/thy_syntax.ML Fri Sep 02 16:57:51 2011 -0700
9.2 +++ b/src/Pure/Thy/thy_syntax.ML Fri Sep 02 16:58:00 2011 -0700
9.3 @@ -16,7 +16,6 @@
9.4 type span
9.5 val span_kind: span -> span_kind
9.6 val span_content: span -> Token.T list
9.7 - val span_range: span -> Position.range
9.8 val span_source: (Token.T, 'a) Source.source -> (span, (Token.T, 'a) Source.source) Source.source
9.9 val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
9.10 val present_span: span -> Output.output
9.11 @@ -101,15 +100,6 @@
9.12 fun span_kind (Span (k, _)) = k;
9.13 fun span_content (Span (_, toks)) = toks;
9.14
9.15 -fun span_range span =
9.16 - (case span_content span of
9.17 - [] => (Position.none, Position.none)
9.18 - | toks =>
9.19 - let
9.20 - val start_pos = Token.position_of (hd toks);
9.21 - val end_pos = Token.end_position_of (List.last toks);
9.22 - in (start_pos, end_pos) end);
9.23 -
9.24
9.25 (* parse *)
9.26
10.1 --- a/src/Tools/jEdit/src/text_area_painter.scala Fri Sep 02 16:57:51 2011 -0700
10.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala Fri Sep 02 16:58:00 2011 -0700
10.3 @@ -201,6 +201,7 @@
10.4 x + w < clip_rect.x + clip_rect.width && chunk.accessable)
10.5 {
10.6 val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
10.7 + val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
10.8 val chunk_font = chunk.style.getFont
10.9 val chunk_color = chunk.style.getForegroundColor
10.10
10.11 @@ -229,7 +230,7 @@
10.12 var x1 = x + w
10.13 gfx.setFont(chunk_font)
10.14 for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
10.15 - val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
10.16 + val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
10.17 gfx.setColor(info.getOrElse(chunk_color))
10.18
10.19 range.try_restrict(caret_range) match {