# HG changeset patch # User wenzelm # Date 1313184568 -7200 # Node ID 21f97048b478eadc4dec59bef97785648c0aa03c # Parent 75ea0e390a92799a31dfb4073e0dc41930301de2# Parent 32e0c150c0103433e9a311fc9427074040888ba2 merged diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/General/exn.ML --- 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 | diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/General/exn.scala --- 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 } diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/General/graph.ML --- 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; diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/General/path.ML --- 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); diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/PIDE/document.ML --- 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 diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/PIDE/document.scala --- 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()) diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/PIDE/isar_document.scala --- 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) diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/System/invoke_scala.scala --- 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)) } } diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/System/session.scala --- 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))) diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/Thy/thy_header.ML --- 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'); diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/Thy/thy_header.scala --- 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)) +} + diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/Thy/thy_info.ML --- 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 diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/Thy/thy_info.scala --- 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 = diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/Thy/thy_load.scala --- 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) } diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/Thy/thy_syntax.scala --- 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)) } diff -r 75ea0e390a92 -r 21f97048b478 src/Pure/library.scala --- 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 } } diff -r 75ea0e390a92 -r 21f97048b478 src/Tools/jEdit/src/document_model.scala --- 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 diff -r 75ea0e390a92 -r 21f97048b478 src/Tools/jEdit/src/plugin.scala --- 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) } } }