# HG changeset patch # User wenzelm # Date 1314997452 -7200 # Node ID 178a6f0ed29d8b8c5800392b68afce27dc8b8947 # Parent f64c715660c3ba4f1b3dfaedbb0df2ab533797cb# Parent c8f1d943bfc5fbddb0bcb45a6a4df961d123bcd8 merged diff -r f64c715660c3 -r 178a6f0ed29d src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Pure/General/markup.ML Fri Sep 02 23:04:12 2011 +0200 @@ -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)]; diff -r f64c715660c3 -r 178a6f0ed29d src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Pure/General/markup.scala Fri Sep 02 23:04:12 2011 +0200 @@ -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 { diff -r f64c715660c3 -r 178a6f0ed29d src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Fri Sep 02 23:04:12 2011 +0200 @@ -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; diff -r f64c715660c3 -r 178a6f0ed29d src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Pure/Isar/token.ML Fri Sep 02 23:04:12 2011 +0200 @@ -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 *) diff -r f64c715660c3 -r 178a6f0ed29d src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Pure/PIDE/document.ML Fri Sep 02 23:04:12 2011 +0200 @@ -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 = diff -r f64c715660c3 -r 178a6f0ed29d src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Fri Sep 02 23:04:12 2011 +0200 @@ -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" diff -r f64c715660c3 -r 178a6f0ed29d src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Fri Sep 02 23:04:12 2011 +0200 @@ -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 } } diff -r f64c715660c3 -r 178a6f0ed29d src/Pure/System/session.scala --- a/src/Pure/System/session.scala Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Pure/System/session.scala Fri Sep 02 23:04:12 2011 +0200 @@ -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) diff -r f64c715660c3 -r 178a6f0ed29d src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.ML Fri Sep 02 23:04:12 2011 +0200 @@ -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 *) diff -r f64c715660c3 -r 178a6f0ed29d src/Tools/jEdit/src/text_area_painter.scala --- a/src/Tools/jEdit/src/text_area_painter.scala Fri Sep 02 19:29:48 2011 +0200 +++ b/src/Tools/jEdit/src/text_area_painter.scala Fri Sep 02 23:04:12 2011 +0200 @@ -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 {