--- a/src/Pure/General/exn.ML Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/General/exn.ML Fri Aug 12 23:29:28 2011 +0200
@@ -30,7 +30,7 @@
structure Exn: EXN =
struct
-(* runtime exceptions as values *)
+(* exceptions as values *)
datatype 'a result =
Res of 'a |
--- a/src/Pure/General/exn.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/General/exn.scala Fri Aug 12 23:29:28 2011 +0200
@@ -9,7 +9,7 @@
object Exn
{
- /* runtime exceptions as values */
+ /* exceptions as values */
sealed abstract class Result[A]
case class Res[A](res: A) extends Result[A]
@@ -24,5 +24,17 @@
case Res(x) => x
case Exn(exn) => throw exn
}
+
+
+ /* message */
+
+ private val runtime_exception = Class.forName("java.lang.RuntimeException")
+
+ def message(exn: Throwable): String =
+ if (exn.getClass == runtime_exception) {
+ val msg = exn.getMessage
+ if (msg == null) "Error" else msg
+ }
+ else exn.toString
}
--- a/src/Pure/General/graph.ML Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/General/graph.ML Fri Aug 12 23:29:28 2011 +0200
@@ -49,6 +49,8 @@
val topological_order: 'a T -> key list
val add_edge_trans_acyclic: key * key -> 'a T -> 'a T (*exception CYCLES*)
val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*)
+ exception DEP of key * key
+ val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list (*exception DEP*)
end;
functor Graph(Key: KEY): GRAPH =
@@ -285,6 +287,24 @@
|> fold add_edge_trans_acyclic (diff_edges G2 G1);
+(* schedule acyclic graph *)
+
+exception DEP of key * key;
+
+fun schedule f G =
+ let
+ val xs = topological_order G;
+ val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
+ let
+ val a = get_node G x;
+ val deps = imm_preds G x |> map (fn y =>
+ (case Table.lookup tab y of
+ SOME b => (y, b)
+ | NONE => raise DEP (x, y)));
+ in Table.update (x, f deps (x, a)) tab end);
+ in map (the o Table.lookup results) xs end;
+
+
(*final declarations of this structure!*)
val map = map_nodes;
val fold = fold_graph;
--- a/src/Pure/General/path.ML Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/General/path.ML Fri Aug 12 23:29:28 2011 +0200
@@ -51,7 +51,7 @@
| check_elem (chs as ["~"]) = err_elem "Illegal" chs
| check_elem (chs as ["~", "~"]) = err_elem "Illegal" chs
| check_elem chs =
- (case inter (op =) ["/", "\\", "$", ":"] chs of
+ (case inter (op =) ["/", "\\", ":"] chs of
[] => chs
| bads => err_elem ("Illegal character(s) " ^ commas_quote bads ^ " in") chs);
--- a/src/Pure/PIDE/document.ML Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/PIDE/document.ML Fri Aug 12 23:29:28 2011 +0200
@@ -249,14 +249,13 @@
in
-fun run_command thy_name raw_tr st =
+fun run_command node_name raw_tr st =
(case
(case Toplevel.init_of raw_tr of
- SOME name => Exn.capture (fn () =>
- let
- val path = Path.explode thy_name;
- val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
- in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
+ SOME name =>
+ 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
--- a/src/Pure/PIDE/document.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/PIDE/document.scala Fri Aug 12 23:29:28 2011 +0200
@@ -51,8 +51,17 @@
case class Edits[A](edits: List[A]) extends Edit[A]
case class Update_Header[A](header: Header) extends Edit[A]
- sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
- val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
+ sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
+ {
+ def norm_deps(f: (String, Path) => String): Header =
+ copy(thy_header =
+ thy_header match {
+ case Exn.Res(header) =>
+ Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
+ case exn => exn
+ })
+ }
+ val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
val empty: Node = Node(empty_header, Map(), Linear_Set())
--- a/src/Pure/PIDE/isar_document.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/PIDE/isar_document.scala Fri Aug 12 23:29:28 2011 +0200
@@ -150,10 +150,10 @@
{ case Document.Node.Remove() => (Nil, Nil) },
{ case Document.Node.Edits(a) => (Nil, list(pair(option(long), option(long)))(a)) },
{ case Document.Node.Update_Header(
- Document.Node.Header(_, Exn.Res(Thy_Header.Header(a, b, c)))) =>
+ Document.Node.Header(_, Exn.Res(Thy_Header(a, b, c)))) =>
(Nil, triple(string, list(string), list(string))(a, b, c)) },
{ case Document.Node.Update_Header(
- Document.Node.Header(_, Exn.Exn(ERROR(a)))) => (List(a), Nil) }))))
+ Document.Node.Header(_, Exn.Exn(e))) => (List(Exn.message(e)), Nil) }))))
YXML.string_of_body(encode(edits)) }
input("Isar_Document.edit_version", Document.ID(old_id), Document.ID(new_id), edits_yxml)
--- a/src/Pure/System/invoke_scala.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/System/invoke_scala.scala Fri Aug 12 23:29:28 2011 +0200
@@ -57,10 +57,8 @@
Exn.capture { f(arg) } match {
case Exn.Res(null) => (Tag.NULL, "")
case Exn.Res(res) => (Tag.OK, res)
- case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
- case Exn.Exn(e) => (Tag.ERROR, e.toString)
+ case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
}
- case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
- case Exn.Exn(e) => (Tag.FAIL, e.toString)
+ case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
}
}
--- a/src/Pure/System/session.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/System/session.scala Fri Aug 12 23:29:28 2011 +0200
@@ -20,7 +20,8 @@
abstract class File_Store
{
- def read(path: Path): String
+ def append(master_dir: String, path: Path): String
+ def require(file: String): Unit
}
@@ -146,7 +147,7 @@
override def is_loaded(name: String): Boolean =
loaded_theories.contains(name)
- override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
+ override def check_thy(dir: Path, name: String): (String, Thy_Header) =
{
val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
@@ -186,7 +187,8 @@
val syntax = current_syntax()
val previous = global_state().history.tip.version
val doc_edits =
- (name, Document.Node.Update_Header[Text.Edit](header)) :: edits.map(edit => (name, edit))
+ (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
+ edits.map(edit => (name, edit))
val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
val change =
global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
--- a/src/Pure/Thy/thy_header.ML Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/Thy/thy_header.ML Fri Aug 12 23:29:28 2011 +0200
@@ -9,7 +9,6 @@
val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
val read: Position.T -> string -> string * string list * (Path.T * bool) list
val thy_path: string -> Path.T
- val split_thy_path: Path.T -> Path.T * string
val consistent_name: string -> string -> unit
end;
@@ -73,11 +72,6 @@
val thy_path = Path.ext "thy" o Path.basic;
-fun split_thy_path path =
- (case Path.split_ext path of
- (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
- | _ => error ("Bad theory file specification: " ^ Path.print path));
-
fun consistent_name name name' =
if name = name' then ()
else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
--- a/src/Pure/Thy/thy_header.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/Thy/thy_header.scala Fri Aug 12 23:29:28 2011 +0200
@@ -25,27 +25,20 @@
val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
- sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
- {
- def map(f: String => String): Header =
- Header(f(name), imports.map(f), uses.map(f))
- }
+
+ /* theory file name */
+ private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
- /* file name */
+ def thy_name(s: String): Option[String] =
+ s match { case Thy_Name(name) => Some(name) case _ => None }
def thy_path(name: String): Path = Path.basic(name).ext("thy")
- def split_thy_path(path: Path): (Path, String) =
- path.split_ext match {
- case (path1, "thy") => (path1.dir, path1.base.implode)
- case _ => error("Bad theory file specification: " + path)
- }
-
/* header */
- val header: Parser[Header] =
+ val header: Parser[Thy_Header] =
{
val file_name = atom("file name", _.is_name)
val theory_name = atom("theory name", _.is_name)
@@ -57,7 +50,7 @@
val args =
theory_name ~ (keyword(IMPORTS) ~! (rep1(theory_name) ~ uses ~ keyword(BEGIN))) ^^
- { case x ~ (_ ~ (ys ~ zs ~ _)) => Header(x, ys, zs) }
+ { case x ~ (_ ~ (ys ~ zs ~ _)) => Thy_Header(x, ys, zs) }
(keyword(HEADER) ~ tags) ~!
((doc_source ~ rep(keyword(";")) ~ keyword(THEORY) ~ tags) ~> args) ^^ { case _ ~ x => x } |
@@ -67,7 +60,7 @@
/* read -- lazy scanning */
- def read(reader: Reader[Char]): Header =
+ def read(reader: Reader[Char]): Thy_Header =
{
val token = lexicon.token(_ => false)
val toks = new mutable.ListBuffer[Token]
@@ -89,10 +82,10 @@
}
}
- def read(source: CharSequence): Header =
+ def read(source: CharSequence): Thy_Header =
read(new CharSequenceReader(source))
- def read(file: File): Header =
+ def read(file: File): Thy_Header =
{
val reader = Scan.byte_reader(file)
try { read(reader).map(Standard_System.decode_permissive_utf8) }
@@ -102,7 +95,7 @@
/* check */
- def check(name: String, source: CharSequence): Header =
+ def check(name: String, source: CharSequence): Thy_Header =
{
val header = read(source)
val name1 = header.name
@@ -111,3 +104,14 @@
header
}
}
+
+
+sealed case class Thy_Header(val name: String, val imports: List[String], val uses: List[String])
+{
+ def map(f: String => String): Thy_Header =
+ Thy_Header(f(name), imports.map(f), uses.map(f))
+
+ def norm_deps(f: String => String): Thy_Header =
+ copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f))
+}
+
--- a/src/Pure/Thy/thy_info.ML Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/Thy/thy_info.ML Fri Aug 12 23:29:28 2011 +0200
@@ -178,51 +178,37 @@
fun task_finished (Task _) = false
| task_finished (Finished _) = true;
+fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents;
+
local
fun finish_thy ((thy, present, commit): result) =
(Global_Theory.join_proofs thy; Future.join present; commit (); thy);
-fun schedule_seq task_graph =
- ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
- (case Graph.get_node task_graph name of
- Task (parents, body) =>
- let val result = body (map (the o Symtab.lookup tab) parents)
- in Symtab.update (name, finish_thy result) tab end
- | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
-
-fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
- let
- val tasks = Graph.topological_order task_graph;
- val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
- (case Graph.get_node task_graph name of
- Task (parents, body) =>
- let
- val get = the o Symtab.lookup tab;
- val deps = map (`get) (Graph.imm_preds task_graph name);
- val task_deps = map (Future.task_of o #1) deps;
- fun failed (future, parent) = if can Future.join future then NONE else SOME parent;
+val schedule_seq =
+ Graph.schedule (fn deps => fn (_, task) =>
+ (case task of
+ Task (parents, body) => finish_thy (body (task_parents deps parents))
+ | Finished thy => thy)) #> ignore;
- val future =
- singleton
- (Future.forks
- {name = "theory:" ^ name, group = NONE, deps = task_deps, pri = 0,
- interrupts = true})
- (fn () =>
- (case map_filter failed deps of
- [] => body (map (#1 o Future.join o get) parents)
- | bad => error (loader_msg ("failed to load " ^ quote name ^
- " (unresolved " ^ commas_quote bad ^ ")") [])));
- in Symtab.update (name, future) tab end
- | Finished thy => Symtab.update (name, Future.value (thy, Future.value (), I)) tab));
- val _ =
- tasks |> maps (fn name =>
- let
- val result = Future.join (the (Symtab.lookup futures name));
- val _ = finish_thy result;
- in [] end handle exn => [Exn.Exn exn])
- |> rev |> Exn.release_all;
- in () end) ();
+val schedule_futures = uninterruptible (fn _ =>
+ Graph.schedule (fn deps => fn (name, task) =>
+ (case task of
+ Task (parents, body) =>
+ singleton
+ (Future.forks
+ {name = "theory:" ^ name, group = NONE,
+ deps = map (Future.task_of o #2) deps,
+ pri = 0, interrupts = true})
+ (fn () =>
+ (case filter (not o can Future.join o #2) deps of
+ [] => body (map (#1 o Future.join) (task_parents deps parents))
+ | bad =>
+ error (loader_msg ("failed to load " ^ quote name ^
+ " (unresolved " ^ commas_quote (map #1 bad) ^ ")") [])))
+ | Finished thy => Future.value (thy, Future.value (), I)))
+ #> maps (fn result => (finish_thy (Future.join result); []) handle exn => [Exn.Exn exn])
+ #> rev #> Exn.release_all) #> ignore;
in
--- a/src/Pure/Thy/thy_info.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/Thy/thy_info.scala Fri Aug 12 23:29:28 2011 +0200
@@ -38,7 +38,7 @@
/* dependencies */
- type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header)
+ type Deps = Map[String, Exn.Result[(String, Thy_Header)]] // name -> (text, header)
private def require_thys(ignored: String => Boolean,
initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
--- a/src/Pure/Thy/thy_load.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/Thy/thy_load.scala Fri Aug 12 23:29:28 2011 +0200
@@ -10,6 +10,6 @@
{
def is_loaded(name: String): Boolean
- def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
+ def check_thy(dir: Path, name: String): (String, Thy_Header)
}
--- a/src/Pure/Thy/thy_syntax.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/Thy/thy_syntax.scala Fri Aug 12 23:29:28 2011 +0200
@@ -203,9 +203,9 @@
val node = nodes(name)
val update_header =
(node.header.thy_header, header) match {
- case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header)))
- if thy_header0 != thy_header => true
- case (Exn.Exn(_), Document.Node.Header(_, Exn.Res(thy_header))) => true
+ case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) =>
+ thy_header0 != thy_header
+ case _ => true
}
if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
}
--- a/src/Pure/library.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Pure/library.scala Fri Aug 12 23:29:28 2011 +0200
@@ -20,19 +20,12 @@
{
/* user errors */
- private val runtime_exception = Class.forName("java.lang.RuntimeException")
-
object ERROR
{
def apply(message: String): Throwable = new RuntimeException(message)
def unapply(exn: Throwable): Option[String] =
exn match {
- case e: RuntimeException =>
- if (e.getClass != runtime_exception) Some(e.toString)
- else {
- val msg = e.getMessage
- Some(if (msg == null) "Error" else msg)
- }
+ case e: RuntimeException => Some(Exn.message(e))
case _ => None
}
}
--- a/src/Tools/jEdit/src/document_model.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Tools/jEdit/src/document_model.scala Fri Aug 12 23:29:28 2011 +0200
@@ -45,10 +45,11 @@
}
}
- def init(session: Session, buffer: Buffer, master_dir: Path, thy_name: String): Document_Model =
+ def init(session: Session, buffer: Buffer,
+ master_dir: String, node_name: String, thy_name: String): Document_Model =
{
exit(buffer)
- val model = new Document_Model(session, buffer, master_dir, thy_name)
+ val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
buffer.setProperty(key, model)
model.activate()
model
@@ -56,15 +57,13 @@
}
-class Document_Model(val session: Session,
- val buffer: Buffer, val master_dir: Path, val thy_name: String)
+class Document_Model(val session: Session, val buffer: Buffer,
+ val master_dir: String, val node_name: String, val thy_name: String)
{
/* pending text edits */
- private val node_name = (master_dir + Path.basic(thy_name)).implode
-
- private def node_header(): Document.Node.Header =
- Document.Node.Header(Path.current, // FIXME master_dir (!?)
+ def node_header(): Document.Node.Header =
+ Document.Node.Header(master_dir,
Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
private object pending_edits // owned by Swing thread
--- a/src/Tools/jEdit/src/plugin.scala Fri Aug 12 09:17:30 2011 -0700
+++ b/src/Tools/jEdit/src/plugin.scala Fri Aug 12 23:29:28 2011 +0200
@@ -23,6 +23,7 @@
import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
import org.gjt.sp.util.SyntaxUtilities
import org.gjt.sp.util.Log
@@ -185,6 +186,15 @@
def buffer_text(buffer: JEditBuffer): String =
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+ def buffer_path(buffer: Buffer): (String, String) =
+ {
+ val master_dir = buffer.getDirectory
+ val path = buffer.getSymlinkPath
+ if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
+ (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
+ else (master_dir, path)
+ }
+
/* document model and view */
@@ -198,16 +208,11 @@
document_model(buffer) match {
case Some(model) => Some(model)
case None =>
- // FIXME strip protocol prefix of URL
- {
- try {
- Some(Thy_Header.split_thy_path(
- Path.explode(Isabelle_System.posix_path(buffer.getPath))))
- }
- catch { case _ => None }
- } map {
- case (master_dir, thy_name) =>
- Document_Model.init(session, buffer, master_dir, thy_name)
+ 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 None => None
}
}
if (opt_model.isDefined) {
@@ -322,15 +327,20 @@
private val file_store = new Session.File_Store
{
- def read(path: Path): String =
+ def append(master_dir: String, path: Path): String =
{
- val platform_path = Isabelle_System.platform_path(path)
- val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
+ 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))
+ }
- Isabelle.jedit_buffers().find(buffer =>
- MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match {
- case Some(buffer) => Isabelle.buffer_text(buffer)
- case None => Standard_System.read_file(new File(platform_path))
+ def require(canonical_name: String)
+ {
+ Swing_Thread.later {
+ if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
+ jEdit.openFile(null: View, canonical_name)
}
}
}