# HG changeset patch # User haftmann # Date 1232177406 -3600 # Node ID 7178c11b6bc14e4262314c3ee6f30f201578de25 # Parent 793766d4c1b5d13532f5d5a200d3e3294885ee59# Parent 0b32c8b84d3e312fec05e0fa682ba175558fccc7 merged diff -r 0b32c8b84d3e -r 7178c11b6bc1 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Sat Jan 17 08:29:54 2009 +0100 +++ b/src/Pure/General/markup.ML Sat Jan 17 08:30:06 2009 +0100 @@ -95,17 +95,7 @@ val editN: string val edit: string -> string -> T val pidN: string val sessionN: string - val classN: string - val messageN: string val message: string -> T val promptN: string val prompt: T - val writelnN: string - val priorityN: string - val tracingN: string - val warningN: string - val errorN: string - val debugN: string - val initN: string - val statusN: string val no_output: output * output val default_output: T -> output * output val add_mode: string -> (T -> output * output) -> unit @@ -284,19 +274,8 @@ val pidN = "pid"; val sessionN = "session"; -val classN = "class"; -val (messageN, message) = markup_string "message" classN; - val (promptN, prompt) = markup_elem "prompt"; -val writelnN = "writeln"; -val priorityN = "priority"; -val tracingN = "tracing"; -val warningN = "warning"; -val errorN = "error"; -val debugN = "debug"; -val initN = "init"; -val statusN = "status"; (* print mode operations *) diff -r 0b32c8b84d3e -r 7178c11b6bc1 src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Sat Jan 17 08:29:54 2009 +0100 +++ b/src/Pure/General/markup.scala Sat Jan 17 08:30:06 2009 +0100 @@ -131,6 +131,21 @@ val SESSION = "session" val MESSAGE = "message" + val CLASS = "class" + + val INIT = "init" + val STATUS = "status" + val WRITELN = "writeln" + val PRIORITY = "priority" + val TRACING = "tracing" + val WARNING = "warning" + val ERROR = "error" + val DEBUG = "debug" + val SYSTEM = "system" + val STDIN = "stdin" + val STDOUT = "stdout" + val SIGNAL = "signal" + val EXIT = "exit" /* content */ diff -r 0b32c8b84d3e -r 7178c11b6bc1 src/Pure/General/yxml.scala --- a/src/Pure/General/yxml.scala Sat Jan 17 08:29:54 2009 +0100 +++ b/src/Pure/General/yxml.scala Sat Jan 17 08:30:06 2009 +0100 @@ -109,12 +109,21 @@ case _ => err("multiple results") } + + /* failsafe parsing */ + + private def markup_failsafe(source: CharSequence) = + XML.Elem (Markup.BAD, Nil, + List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>")))) + + def parse_body_failsafe(source: CharSequence) = { + try { parse_body(source) } + catch { case _: RuntimeException => List(markup_failsafe(source)) } + } + def parse_failsafe(source: CharSequence) = { try { parse(source) } - catch { - case _: RuntimeException => XML.Elem (Markup.BAD, Nil, - List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>")))) - } + catch { case _: RuntimeException => markup_failsafe(source) } } } diff -r 0b32c8b84d3e -r 7178c11b6bc1 src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Sat Jan 17 08:29:54 2009 +0100 +++ b/src/Pure/Isar/isar_document.ML Sat Jan 17 08:30:06 2009 +0100 @@ -24,7 +24,7 @@ type command_id = string; type document_id = string; -fun new_id () = "isabelle:" ^ serial_string (); +fun make_id () = "isabelle:" ^ serial_string (); fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ quote id); fun err_undef kind id = error ("Unknown " ^ kind ^ ": " ^ quote id); @@ -53,7 +53,6 @@ fun set_entry_state (id, state_id) = put_entry_state id (SOME state_id); - (* document *) datatype document = Document of @@ -81,11 +80,11 @@ fun first_entry P (Document {start, entries, ...}) = let - fun find _ NONE = NONE - | find prev (SOME id) = + fun first _ NONE = NONE + | first prev (SOME id) = let val entry = the_entry entries id - in if P (id, entry) then SOME (prev, id) else find (SOME id) (#next entry) end; - in find NONE (SOME start) end; + in if P (id, entry) then SOME (prev, id, entry) else first (SOME id) (#next entry) end; + in first NONE (SOME start) end; (* modify entries *) @@ -135,16 +134,24 @@ end; -fun define_state (id: state_id) state = - change_states (Symtab.update_new (id, state)) +(* state *) + +val empty_state = Future.value (SOME Toplevel.toplevel); + +fun define_state (id: state_id) = + change_states (Symtab.update_new (id, empty_state)) handle Symtab.DUP dup => err_dup "state" dup; +fun put_state (id: state_id) state = change_states (Symtab.update (id, state)); + fun the_state (id: state_id) = (case Symtab.lookup (get_states ()) id of NONE => err_undef "state" id | SOME state => state); +(* command *) + fun define_command id tr = change_commands (Symtab.update_new (id, Toplevel.put_id id tr)) handle Symtab.DUP dup => err_dup "command" dup; @@ -155,6 +162,8 @@ | SOME tr => tr); +(* document *) + fun define_document (id: document_id) document = change_documents (Symtab.update_new (id, document)) handle Symtab.DUP dup => err_dup "document" dup; @@ -162,21 +171,38 @@ fun the_document (id: document_id) = (case Symtab.lookup (get_documents ()) id of NONE => err_undef "document" id - | SOME (Document doc) => doc); + | SOME document => document); + +(** main operations **) + (* begin/end document *) fun begin_document (id: document_id) path = let val (dir, name) = ThyLoad.split_thy_path path; val _ = define_command id Toplevel.empty; - val _ = define_state id (Future.value (SOME Toplevel.toplevel)); + val _ = define_state id; val entries = Symtab.make [(id, make_entry NONE (SOME id))]; val _ = define_document id (make_document dir name id entries); in () end; -fun end_document (id: document_id) = error "FIXME"; +fun end_document (id: document_id) = + let + val document as Document {name, ...} = the_document id; + val end_state = + the_state (the (#state (#3 (the + (first_entry (fn (_, {next, ...}) => is_none next) document))))); + val _ = + Future.fork_deps [end_state] (fn () => + (case Future.join end_state of + SOME st => + (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st; + ThyInfo.touch_child_thys name; + ThyInfo.register_thy name) + | NONE => error ("Failed to finish theory " ^ quote name))); + in () end; (* document editing *) @@ -185,45 +211,24 @@ fun is_changed entries' (id, {next = _, state}) = (case try (the_entry entries') id of - SOME {next = _, state = state'} => state' <> state - | _ => true); - -fun cancel_state (id, {next = _, state = SOME state_id}) () = Future.cancel (the_state state_id) - | cancel_state _ () = (); - -fun update_state tr state state_id' = - Future.fork_deps [state] (fn () => - (case Future.join state of - NONE => NONE - | SOME st => Toplevel.run_command (Toplevel.put_id state_id' tr) st)); - -fun new_state (id, _) (state_id, updates) = - let - val state_id' = new_id (); - val state' = update_state (the_command id) (the_state state_id) state_id'; - val _ = define_state state_id' state'; - in (state_id', (id, state_id') :: updates) end; + NONE => true + | SOME {next = _, state = state'} => state' <> state); -fun update_states old_document new_document = +fun new_state name (id, _) (state_id, updates) = let - fun cancel_old id = fold_entries id cancel_state old_document (); - - val Document {entries = old_entries, ...} = old_document; - val Document {entries = new_entries, ...} = new_document; - in - (case first_entry (is_changed old_entries) new_document of - NONE => - (case first_entry (is_changed new_entries) old_document of - NONE => ([], new_document) - | SOME (_, id) => (cancel_old id; ([], new_document))) - | SOME (prev, id) => - let - val _ = cancel_old id; - val prev_state_id = the (#state (the_entry new_entries (the prev))); - val (_, updates) = fold_entries id new_state new_document (prev_state_id, []); - val new_document' = new_document |> map_entries (fold set_entry_state updates); - in (rev updates, new_document') end) - end; + val state_id' = make_id (); + val _ = define_state state_id'; + val tr = Toplevel.put_id state_id' (the_command id); + fun make_state' () = + let + val state = the_state state_id; + val state' = + Future.fork_deps [state] (fn () => + (case Future.join state of + NONE => NONE + | SOME st => Toplevel.run_command name tr st)); + in put_state state_id' state' end; + in (state_id', ((id, state_id'), make_state') :: updates) end; fun report_updates _ [] = () | report_updates (document_id: document_id) updates = @@ -233,15 +238,33 @@ in -fun edit_document (id: document_id) (id': document_id) edits = +fun edit_document (old_id: document_id) (new_id: document_id) edits = let - val document = Document (the_document id); - val (updates, document') = - document - |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits - |> update_states document; - val _ = define_document id' document'; - val _ = report_updates id' updates; + val old_document as Document {name, entries = old_entries, ...} = the_document old_id; + val new_document as Document {entries = new_entries, ...} = old_document + |> fold (fn (id, SOME id2) => insert_after id id2 | (id, NONE) => delete_after id) edits; + + fun cancel_old id = fold_entries id + (fn (_, {state = SOME state_id, ...}) => K (Future.cancel (the_state state_id)) | _ => K ()) + old_document (); + + val (updates, new_document') = + (case first_entry (is_changed old_entries) new_document of + NONE => + (case first_entry (is_changed new_entries) old_document of + NONE => ([], new_document) + | SOME (_, id, _) => (cancel_old id; ([], new_document))) + | SOME (prev, id, _) => + let + val _ = cancel_old id; + val prev_state_id = the (#state (the_entry new_entries (the prev))); + val (_, updates) = fold_entries id (new_state name) new_document (prev_state_id, []); + val new_document' = new_document |> map_entries (fold (set_entry_state o #1) updates); + in (rev updates, new_document') end); + + val _ = define_document new_id new_document'; + val _ = report_updates new_id (map #1 updates); + val _ = List.app (fn (_, run) => run ()) updates; in () end; end; diff -r 0b32c8b84d3e -r 7178c11b6bc1 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Jan 17 08:29:54 2009 +0100 +++ b/src/Pure/Isar/toplevel.ML Sat Jan 17 08:30:06 2009 +0100 @@ -96,7 +96,7 @@ val transition: bool -> transition -> state -> (state * (exn * string) option) option val commit_exit: Position.T -> transition val command: transition -> state -> state - val run_command: transition -> state -> state option + val run_command: string -> transition -> state -> state option val excursion: (transition * transition list) list -> (transition * state) list lazy end; @@ -698,11 +698,17 @@ let val st' = command tr st in (st', st') end; -fun run_command tr st = - (case transition true tr st of - SOME (st', NONE) => (status tr Markup.finished; SOME st') - | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE) - | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE)); +fun run_command thy_name tr st = + (case + (case init_of tr of + SOME name => Exn.capture (fn () => ThyLoad.check_name thy_name name) () + | NONE => Exn.Result ()) of + Exn.Result () => + (case transition true tr st of + SOME (st', NONE) => (status tr Markup.finished; SOME st') + | SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE) + | NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE)) + | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE)); (* excursion of units, consisting of commands with proof *) diff -r 0b32c8b84d3e -r 7178c11b6bc1 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Sat Jan 17 08:29:54 2009 +0100 +++ b/src/Pure/Thy/thy_load.ML Sat Jan 17 08:30:06 2009 +0100 @@ -25,6 +25,7 @@ val check_file: Path.T -> Path.T -> (Path.T * File.ident) option val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option val check_thy: Path.T -> string -> Path.T * File.ident + val check_name: string -> string -> unit val deps_thy: Path.T -> string -> {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list} val load_ml: Path.T -> Path.T -> Path.T * File.ident @@ -95,6 +96,11 @@ | SOME thy_id => thy_id) end; +fun check_name name name' = + if name = name' then () + else error ("Filename " ^ quote (Path.implode (thy_path name)) ^ + " does not agree with theory name " ^ quote name'); + (* theory deps *) @@ -104,9 +110,7 @@ val text = explode (File.read path); val (name', imports, uses) = ThyHeader.read (Path.position path) (Source.of_list_limited 8000 text); - val _ = name = name' orelse - error ("Filename " ^ quote (Path.implode (Path.base path)) ^ - " does not agree with theory name " ^ quote name'); + val _ = check_name name name'; val uses = map (Path.explode o #1) uses; in {master = master, text = text, imports = imports, uses = uses} end; diff -r 0b32c8b84d3e -r 7178c11b6bc1 src/Pure/Tools/isabelle_process.ML --- a/src/Pure/Tools/isabelle_process.ML Sat Jan 17 08:29:54 2009 +0100 +++ b/src/Pure/Tools/isabelle_process.ML Sat Jan 17 08:30:06 2009 +0100 @@ -55,9 +55,6 @@ let val clean = clean_string [Symbol.STX, "\n", "\r"] in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end; -fun message_text class body = - YXML.element Markup.messageN [(Markup.classN, class)] [clean_string [Symbol.STX] body]; - fun message_pos trees = trees |> get_first (fn XML.Elem (name, atts, ts) => if name = Markup.positionN then SOME (Position.of_properties atts) @@ -69,21 +66,21 @@ in -fun message _ _ _ "" = () - | message out_stream ch class body = +fun message _ _ "" = () + | message out_stream ch body = let val pos = the_default Position.none (message_pos (YXML.parse_body body)); val props = Position.properties_of (Position.thread_data ()) |> Position.default_properties pos; - val txt = message_text class body; + val txt = clean_string [Symbol.STX] body; in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end; fun init_message out_stream = let val pid = (Markup.pidN, process_id ()); val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown"); - val text = message_text Markup.initN (Session.welcome ()); + val text = Session.welcome (); in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end; end; @@ -116,13 +113,13 @@ val _ = SimpleThread.fork false (auto_flush out_stream); val _ = SimpleThread.fork false (auto_flush TextIO.stdErr); in - Output.status_fn := message out_stream "B" Markup.statusN; - Output.writeln_fn := message out_stream "C" Markup.writelnN; - Output.priority_fn := message out_stream "D" Markup.priorityN; - Output.tracing_fn := message out_stream "E" Markup.tracingN; - Output.warning_fn := message out_stream "F" Markup.warningN; - Output.error_fn := message out_stream "G" Markup.errorN; - Output.debug_fn := message out_stream "H" Markup.debugN; + Output.status_fn := message out_stream "B"; + Output.writeln_fn := message out_stream "C"; + Output.priority_fn := message out_stream "D"; + Output.tracing_fn := message out_stream "E"; + Output.warning_fn := message out_stream "F"; + Output.error_fn := message out_stream "G"; + Output.debug_fn := message out_stream "H"; Output.prompt_fn := ignore; out_stream end; diff -r 0b32c8b84d3e -r 7178c11b6bc1 src/Pure/Tools/isabelle_process.scala --- a/src/Pure/Tools/isabelle_process.scala Sat Jan 17 08:29:54 2009 +0100 +++ b/src/Pure/Tools/isabelle_process.scala Sat Jan 17 08:30:06 2009 +0100 @@ -50,6 +50,21 @@ ('2' : Int) -> Kind.STDOUT, ('3' : Int) -> Kind.SIGNAL, ('4' : Int) -> Kind.EXIT) + // message markup + val markup = Map( + Kind.INIT -> Markup.INIT, + Kind.STATUS -> Markup.STATUS, + Kind.WRITELN -> Markup.WRITELN, + Kind.PRIORITY -> Markup.PRIORITY, + Kind.TRACING -> Markup.TRACING, + Kind.WARNING -> Markup.WARNING, + Kind.ERROR -> Markup.ERROR, + Kind.DEBUG -> Markup.DEBUG, + Kind.SYSTEM -> Markup.SYSTEM, + Kind.STDIN -> Markup.STDIN, + Kind.STDOUT -> Markup.STDOUT, + Kind.SIGNAL -> Markup.SIGNAL, + Kind.EXIT -> Markup.EXIT) //}}} def is_raw(kind: Value) = kind == STDOUT @@ -67,8 +82,10 @@ class Result(val kind: Kind.Value, val props: Properties, val result: String) { override def toString = { - val tree = YXML.parse_failsafe(result) - val res = if (kind == Kind.STATUS) tree.toString else XML.content(tree).mkString + val trees = YXML.parse_body_failsafe(result) + val res = + if (kind == Kind.STATUS) trees.map(_.toString).mkString + else trees.flatMap(XML.content(_).mkString).mkString if (props == null) kind.toString + " [[" + res + "]]" else kind.toString + " " + props.toString + " [[" + res + "]]" } @@ -77,6 +94,10 @@ def is_system = Kind.is_system(kind) } + def parse_message(kind: Kind.Value, result: String) = { + XML.Elem(Markup.MESSAGE, List((Markup.CLASS, Kind.markup(kind))), + YXML.parse_body_failsafe(result)) + } }