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;
--- 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;
--- 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);
--- 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]
--- 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;
--- 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)) }
--- 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*)
--- 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 =>
--- 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)))
}
--- 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)) =>
--- 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)