# HG changeset patch # User wenzelm # Date 1313259636 -7200 # Node ID 05641edb5d308ff1e80d0c16540d1d87b8965e37 # Parent 49501dc1a7b8569c98da95bee5846f5efd331894 provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment; diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/Isar/toplevel.ML Sat Aug 13 20:20:36 2011 +0200 @@ -34,7 +34,7 @@ val thread: bool -> (unit -> unit) -> Thread.thread type transition val empty: transition - val init_of: transition -> string option + val is_init: transition -> bool val print_of: transition -> bool val name_of: transition -> string val pos_of: transition -> Position.T @@ -356,7 +356,8 @@ fun get_init (Transition {trans = [Init args], ...}) = SOME args | get_init _ = NONE; -val init_of = Option.map #2 o get_init; +val is_init = is_some o get_init; + fun print_of (Transition {print, ...}) = print; fun name_of (Transition {name, ...}) = name; fun pos_of (Transition {pos, ...}) = pos; diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/PIDE/document.ML Sat Aug 13 20:20:36 2011 +0200 @@ -15,9 +15,9 @@ val new_id: unit -> id val parse_id: string -> id val print_id: id -> string - type node_header = (string * string list * string list) Exn.result + type node_header = (string * string list * (string * bool) list) Exn.result datatype node_edit = - Remove | + Clear | Edits of (command_id option * command_id option) list | Header of node_header type edit = string * node_edit @@ -55,7 +55,7 @@ (** document structure **) -type node_header = (string * string list * string list) Exn.result; +type node_header = (string * string list * (string * bool) list) Exn.result; structure Entries = Linear_Set(type key = command_id val ord = int_ord); abstype node = Node of @@ -82,13 +82,17 @@ fun set_last last = map_node (fn (header, entries, _) => (header, entries, last)); val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id); -val empty_version = Version Graph.empty; +val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id)); + +fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; +fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes; +fun update_node name f = Graph.default_node (name, empty_node) #> Graph.map_node name f; (* node edits and associated executions *) datatype node_edit = - Remove | + Clear | Edits of (command_id option * command_id option) list | Header of node_header; @@ -114,22 +118,30 @@ (* version operations *) +val empty_version = Version Graph.empty; + fun nodes_of (Version nodes) = nodes; +val node_of = get_node o nodes_of; val node_names_of = Graph.keys o nodes_of; -fun get_node version name = Graph.get_node (nodes_of version) name - handle Graph.UNDEF _ => empty_node; - -fun update_node name f = - Graph.default_node (name, empty_node) #> Graph.map_node name f; +fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); fun edit_nodes (name, node_edit) (Version nodes) = Version (case node_edit of - Remove => perhaps (try (Graph.del_node name)) nodes + Clear => update_node name clear_node nodes | Edits edits => update_node name (edit_node edits) nodes - (* FIXME maintain deps; cycles!? *) - | Header header => update_node name (set_header header) nodes); + | Header header => + let + val node = get_node nodes name; + val nodes' = Graph.new_node (name, node) (remove_node name nodes); + val parents = + (case header of Exn.Res (_, parents, _) => parents | _ => []) + |> filter (can (Graph.get_node nodes')); + val (header', nodes'') = + (header, Graph.add_deps_acyclic (name, parents) nodes') + handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes'); + in Graph.map_node name (set_header header') nodes'' end); fun put_node name node (Version nodes) = Version (nodes @@ -214,11 +226,11 @@ fun get_theory state version_id pos name = let - val last = get_last (get_node (the_version state version_id) name); + val last = get_last (node_of (the_version state version_id) name); val st = (case Lazy.peek (the_exec state last) of SOME result => #2 (Exn.release result) - | NONE => error ("Unfinished execution for theory " ^ quote name)); + | NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos)); in Toplevel.end_theory pos st end; @@ -263,41 +275,38 @@ in -fun run_command node_name raw_tr st = - (case - (case Toplevel.init_of raw_tr of - SOME _ => - Exn.capture (fn () => - let val master_dir = Path.dir (Path.explode node_name); (* FIXME move to Scala side *) - in Toplevel.modify_master (SOME master_dir) raw_tr end) () - | NONE => Exn.Res raw_tr) of - Exn.Res tr => - let - val is_init = is_some (Toplevel.init_of tr); - val is_proof = Keyword.is_proof (Toplevel.name_of tr); - val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof); +fun run_command (node_name, node_header) raw_tr st = + let + val is_init = Toplevel.is_init raw_tr; + val tr = + if is_init then + raw_tr |> Toplevel.modify_init (fn _ => + let + (* FIXME get theories from document state *) + (* FIXME provide files via Scala layer *) + val (name, imports, uses) = Exn.release node_header; + val master = SOME (Path.dir (Path.explode node_name)); + in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end) + else raw_tr; - val start = Timing.start (); - val (errs, result) = - if Toplevel.is_toplevel st andalso not is_init then ([], SOME st) - else run (is_init orelse is_proof) (Toplevel.set_print false tr) st; - val _ = timing tr (Timing.result start); - val _ = List.app (Toplevel.error_msg tr) errs; - val res = - (case result of - NONE => (Toplevel.status tr Markup.failed; (false, st)) - | SOME st' => - (Toplevel.status tr Markup.finished; - proof_status tr st'; - if do_print then async_state tr st' else (); - (true, st'))); - in res end - | Exn.Exn exn => - if Exn.is_interrupt exn then reraise exn - else - (Toplevel.error_msg raw_tr (ML_Compiler.exn_message exn); - Toplevel.status raw_tr Markup.failed; - (false, Toplevel.toplevel))); + val is_proof = Keyword.is_proof (Toplevel.name_of tr); + val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof); + + val start = Timing.start (); + val (errs, result) = + if Toplevel.is_toplevel st andalso not is_init then ([], SOME st) + else run (is_init orelse is_proof) (Toplevel.set_print false tr) st; + val _ = timing tr (Timing.result start); + val _ = List.app (Toplevel.error_msg tr) errs; + in + (case result of + NONE => (Toplevel.status tr Markup.failed; (false, st)) + | SOME st' => + (Toplevel.status tr Markup.finished; + proof_status tr st'; + if do_print then async_state tr st' else (); + (true, st'))) + end; end; @@ -315,7 +324,7 @@ NONE => true | SOME exec' => exec' <> exec); -fun new_exec name (id: command_id) (exec_id, updates, state) = +fun new_exec node_info (id: command_id) (exec_id, updates, state) = let val exec = the_exec state exec_id; val exec_id' = new_id (); @@ -325,7 +334,7 @@ let val st = #2 (Lazy.force exec); val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr); - in run_command name exec_tr st end); + in run_command node_info exec_tr st end); val state' = define_exec exec_id' exec' state; in (exec_id', (id, exec_id') :: updates, state') end; @@ -338,8 +347,11 @@ val new_version = fold edit_nodes edits old_version; fun update_node name (rev_updates, version, st) = - let val node = get_node version name in - (case first_entry NONE (is_changed (get_node old_version name)) node of + let + val node = node_of version name; + val header = get_header node; + in + (case first_entry NONE (is_changed (node_of old_version name)) node of NONE => (rev_updates, version, st) | SOME ((prev, id), _) => let @@ -348,12 +360,12 @@ NONE => no_id | SOME prev_id => the_default no_id (the_entry node prev_id)); val (last, rev_upds, st') = - fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st); + fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st); val node' = node |> fold update_entry rev_upds |> set_last last; in (rev_upds @ rev_updates, put_node name node' version, st') end) end; - (* FIXME proper node deps *) + (* FIXME Graph.schedule *) val (rev_updates, new_version', state') = fold update_node (node_names_of new_version) ([], new_version, state); val state'' = define_version new_id new_version' state'; @@ -380,7 +392,7 @@ [fn () => node_names_of version |> List.app (fn name => fold_entries NONE (fn (_, exec) => fn () => force_exec exec) - (get_node version name) ())]; + (node_of version name) ())]; in (versions, commands, execs, execution') end); diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/PIDE/document.scala Sat Aug 13 20:20:36 2011 +0200 @@ -44,12 +44,12 @@ { def map[B](f: A => B): Edit[B] = this match { - case Remove() => Remove() + case Clear() => Clear() case Edits(es) => Edits(es.map(f)) case Header(header) => Header(header) } } - case class Remove[A]() extends Edit[A] + case class Clear[A]() extends Edit[A] case class Edits[A](edits: List[A]) extends Edit[A] case class Header[A](header: Node_Header) extends Edit[A] diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/PIDE/isar_document.ML --- a/src/Pure/PIDE/isar_document.ML Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/PIDE/isar_document.ML Sat Aug 13 20:20:36 2011 +0200 @@ -22,10 +22,11 @@ let open XML.Decode in list (pair string (variant - [fn ([], []) => Document.Remove, + [fn ([], []) => Document.Clear, fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), fn ([], a) => - Document.Header (Exn.Res (triple string (list string) (list string) a)), + Document.Header + (Exn.Res (triple string (list string) (list (pair string bool)) a)), fn ([a], []) => Document.Header (Exn.Exn (ERROR a))])) end; diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/PIDE/isar_document.scala Sat Aug 13 20:20:36 2011 +0200 @@ -147,10 +147,10 @@ def encode: T[List[Document.Edit_Command_ID]] = list(pair(string, variant(List( - { case Document.Node.Remove() => (Nil, Nil) }, + { case Document.Node.Clear() => (Nil, Nil) }, { case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) }, { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) => - (Nil, triple(string, list(string), list(string))(a, b, c)) }, + (Nil, triple(string, list(string), list(pair(string, bool)))(a, b, c)) }, { case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) })))) YXML.string_of_body(encode(edits)) } diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/ROOT.ML Sat Aug 13 20:20:36 2011 +0200 @@ -243,10 +243,10 @@ use "Thy/thy_output.ML"; use "Thy/thy_syntax.ML"; use "Isar/outer_syntax.ML"; -use "PIDE/document.ML"; use "Thy/present.ML"; use "Thy/thy_load.ML"; use "Thy/thy_info.ML"; +use "PIDE/document.ML"; use "Thy/rail.ML"; (*theory and proof operations*) diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/System/session.scala Sat Aug 13 20:20:36 2011 +0200 @@ -188,13 +188,14 @@ { val syntax = current_syntax() val previous = global_state().history.tip.version + val norm_header = Document.Node.norm_header[Text.Edit]( name => file_store.append(master_dir, Path.explode(name)), header) - val doc_edits = (name, norm_header) :: edits.map(edit => (name, edit)) - val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) } + val text_edits = (name, norm_header) :: edits.map(edit => (name, edit)) + val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) } val change = - global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2))) + global_state.change_yield(_.extend_history(previous, text_edits, result.map(_._2))) result.map { case (doc_edits, _) => @@ -331,7 +332,7 @@ case Init_Node(name, master_dir, header, text) if prover.isDefined => // FIXME compare with existing node handle_edits(name, master_dir, header, - List(Document.Node.Remove(), Document.Node.Edits(List(Text.Edit.insert(0, text))))) + List(Document.Node.Clear(), Document.Node.Edits(List(Text.Edit.insert(0, text))))) reply(()) case Edit_Node(name, master_dir, header, text_edits) if prover.isDefined => diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/Thy/thy_header.scala Sat Aug 13 20:20:36 2011 +0200 @@ -28,10 +28,10 @@ /* theory file name */ - private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""") + private val Thy_Name = new Regex("""(.*?)([^/\\:]+)\.thy""") - def thy_name(s: String): Option[String] = - s match { case Thy_Name(name) => Some(name) case _ => None } + def thy_name(s: String): Option[(String, String)] = + s match { case Thy_Name(prefix, name) => Some((prefix, name)) case _ => None } def thy_path(name: String): Path = Path.basic(name).ext("thy") @@ -44,7 +44,8 @@ val theory_name = atom("theory name", _.is_name) val file = - keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name + keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => (x, false) } | + file_name ^^ (x => (x, true)) val uses = opt(keyword(USES) ~! (rep1(file))) ^^ { case None => Nil case Some(_ ~ xs) => xs } @@ -106,12 +107,13 @@ } -sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String]) +sealed case class Thy_Header( + val name: String, val imports: List[String], val uses: List[(String, Boolean)]) { def map(f: String => String): Thy_Header = - Thy_Header(f(name), imports.map(f), uses.map(f)) + Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2))) def norm_deps(f: String => String): Thy_Header = - copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f)) + copy(imports = imports.map(name => f(name)), uses = uses.map(p => (f(p._1), p._2))) } diff -r 49501dc1a7b8 -r 05641edb5d30 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Sat Aug 13 20:20:36 2011 +0200 @@ -179,8 +179,8 @@ var nodes = previous.nodes edits foreach { - case (name, Document.Node.Remove()) => - doc_edits += (name -> Document.Node.Remove()) + case (name, Document.Node.Clear()) => + doc_edits += (name -> Document.Node.Clear()) nodes -= name case (name, Document.Node.Edits(text_edits)) => diff -r 49501dc1a7b8 -r 05641edb5d30 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sat Aug 13 16:07:26 2011 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Sat Aug 13 20:20:36 2011 +0200 @@ -210,8 +210,8 @@ case None => val (master_dir, path) = buffer_path(buffer) Thy_Header.thy_name(path) match { - case Some(name) => - Some(Document_Model.init(session, buffer, master_dir, path, name)) + case Some((prefix, name)) => + Some(Document_Model.init(session, buffer, master_dir, prefix + name, name)) case None => None } } @@ -327,13 +327,17 @@ private val file_store = new Session.File_Store { - def append(master_dir: String, path: Path): String = + def append(master_dir: String, source_path: Path): String = { - val vfs = VFSManager.getVFSForPath(master_dir) - if (vfs.isInstanceOf[FileVFS]) - MiscUtilities.resolveSymlinks( - vfs.constructPath(master_dir, Isabelle_System.platform_path(path))) - else vfs.constructPath(master_dir, Isabelle_System.standard_path(path)) + val path = source_path.expand + if (path.is_absolute) Isabelle_System.platform_path(path) + else { + val vfs = VFSManager.getVFSForPath(master_dir) + if (vfs.isInstanceOf[FileVFS]) + MiscUtilities.resolveSymlinks( + vfs.constructPath(master_dir, Isabelle_System.platform_path(path))) + else vfs.constructPath(master_dir, Isabelle_System.standard_path(path)) + } } def require(canonical_name: String)