--- a/src/Pure/General/path.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/General/path.scala Mon Jul 04 16:54:58 2011 +0200
@@ -19,7 +19,7 @@
private case object Parent extends Elem
private def err_elem(msg: String, s: String): Nothing =
- error (msg + " path element specification: " + Library.quote(s))
+ error (msg + " path element specification: " + quote(s))
private def check_elem(s: String): String =
if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
@@ -27,7 +27,7 @@
s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
case Nil => s
case bads =>
- err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s)
+ err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
}
private def root_elem(s: String): Elem = Root(check_elem(s))
@@ -114,7 +114,7 @@
case _ => elems.map(Path.implode_elem).reverse.mkString("/")
}
- override def toString: String = Library.quote(implode)
+ override def toString: String = quote(implode)
/* base element */
--- a/src/Pure/General/yxml.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/General/yxml.scala Mon Jul 04 16:54:58 2011 +0200
@@ -144,12 +144,12 @@
def parse_body_failsafe(source: CharSequence): XML.Body =
{
try { parse_body(source) }
- catch { case _: RuntimeException => List(markup_failsafe(source)) }
+ catch { case ERROR(_) => List(markup_failsafe(source)) }
}
def parse_failsafe(source: CharSequence): XML.Tree =
{
try { parse(source) }
- catch { case _: RuntimeException => markup_failsafe(source) }
+ catch { case ERROR(_) => markup_failsafe(source) }
}
}
--- a/src/Pure/PIDE/document.ML Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/PIDE/document.ML Mon Jul 04 16:54:58 2011 +0200
@@ -80,10 +80,10 @@
NONE => entries
| SOME next => Entries.update (next, NONE) entries);
-fun edit_node (hook, SOME id2) (Node entries) =
- Node (Entries.insert_after hook (id2, NONE) entries)
- | edit_node (hook, NONE) (Node entries) =
- Node (entries |> Entries.delete_after hook |> reset_after hook);
+fun edit_node (id, SOME id2) (Node entries) =
+ Node (Entries.insert_after id (id2, NONE) entries)
+ | edit_node (id, NONE) (Node entries) =
+ Node (entries |> Entries.delete_after id |> reset_after id);
(* version operations *)
--- a/src/Pure/PIDE/text.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/PIDE/text.scala Mon Jul 04 16:54:58 2011 +0200
@@ -46,7 +46,7 @@
def try_restrict(that: Range): Option[Range] =
try { Some (restrict(that)) }
- catch { case _: RuntimeException => None }
+ catch { case ERROR(_) => None }
}
@@ -57,7 +57,7 @@
def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
def try_restrict(r: Text.Range): Option[Info[A]] =
try { Some(Info(range.restrict(r), info)) }
- catch { case _: RuntimeException => None }
+ catch { case ERROR(_) => None }
}
--- a/src/Pure/System/cygwin.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/System/cygwin.scala Mon Jul 04 16:54:58 2011 +0200
@@ -115,7 +115,7 @@
try {
Download.file(parent, "Downloading", new URL("http://www.cygwin.com/setup.exe"), setup_exe)
}
- catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
+ catch { case ERROR(_) => error("Failed to download Cygwin setup program") }
val (_, rc) = Standard_System.raw_exec(root, null, true,
setup_exe.toString, "-R", root.toString, "-l", download.toString,
--- a/src/Pure/System/gui_setup.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/System/gui_setup.scala Mon Jul 04 16:54:58 2011 +0200
@@ -51,9 +51,7 @@
if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
- } catch {
- case e: RuntimeException => text.append(e.getMessage + "\n")
- }
+ } catch { case ERROR(msg) => text.append(msg + "\n") }
// reactions
listenTo(ok)
--- a/src/Pure/System/session.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/System/session.scala Mon Jul 04 16:54:58 2011 +0200
@@ -2,7 +2,7 @@
Author: Makarius
Options: :folding=explicit:collapseFolds=1:
-Isabelle session, potentially with running prover.
+Main Isabelle/Scala session, potentially with running prover process.
*/
package isabelle
@@ -16,6 +16,14 @@
object Session
{
+ /* abstract file store */
+
+ abstract class File_Store
+ {
+ def read(path: Path): String
+ }
+
+
/* events */
case object Global_Settings
@@ -32,7 +40,7 @@
}
-class Session(val system: Isabelle_System)
+class Session(val system: Isabelle_System, val file_store: Session.File_Store)
{
/* real time parameters */ // FIXME properties or settings (!?)
@@ -116,6 +124,8 @@
/** main protocol actor **/
+ /* global state */
+
@volatile private var syntax = new Outer_Syntax(system.symbols)
def current_syntax(): Outer_Syntax = syntax
@@ -134,15 +144,41 @@
private val global_state = new Volatile(Document.State.init)
def current_state(): Document.State = global_state.peek()
+
+ /* theory files */
+
+ val thy_header = new Thy_Header(system.symbols)
+
+ val thy_load = new Thy_Load
+ {
+ override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
+ {
+ val file = system.platform_file(dir + Thy_Header.thy_path(name))
+ if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
+ val text = Standard_System.read_file(file)
+ val header = thy_header.read(text)
+ (text, header)
+ }
+ }
+
+ val thy_info = new Thy_Info(thy_load)
+
+
+ /* actor messages */
+
private case object Interrupt_Prover
- private case class Edit_Version(edits: List[Document.Edit_Text])
+ private case class Edit_Node(thy_name: String,
+ header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
+ private case class Init_Node(thy_name: String,
+ header: Exn.Result[Thy_Header.Header], text: String)
private case class Start(timeout: Time, args: List[String])
var verbose: Boolean = false
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
{
- var prover: Isabelle_Process with Isar_Document = null
+ val this_actor = self
+ var prover: Option[Isabelle_Process with Isar_Document] = None
/* document changes */
@@ -174,7 +210,8 @@
case Some(command) =>
if (global_state.peek().lookup_command(command.id).isEmpty) {
global_state.change(_.define_command(command))
- prover.define_command(command.id, system.symbols.encode(command.source))
+ prover.get.
+ define_command(command.id, system.symbols.encode(command.source))
}
Some(command.id)
}
@@ -183,7 +220,7 @@
(name -> Some(ids))
}
global_state.change(_.define_version(version, former_assignment))
- prover.edit_version(previous.id, version.id, id_edits)
+ prover.get.edit_version(previous.id, version.id, id_edits)
}
//}}}
@@ -241,47 +278,63 @@
//}}}
+ def edit_version(edits: List[Document.Edit_Text])
+ //{{{
+ {
+ val previous = global_state.peek().history.tip.version
+ val syntax = current_syntax()
+ val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) }
+ val change = global_state.change_yield(_.extend_history(previous, edits, result))
+
+ change.version.map(_ => {
+ assignments.await { global_state.peek().is_assigned(previous.get_finished) }
+ this_actor ! change })
+ }
+ //}}}
+
+
/* main loop */
var finished = false
while (!finished) {
receive {
case Interrupt_Prover =>
- if (prover != null) prover.interrupt
+ prover.map(_.interrupt)
- case Edit_Version(edits) if prover != null =>
- val previous = global_state.peek().history.tip.version
- val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
- val change = global_state.change_yield(_.extend_history(previous, edits, result))
-
- val this_actor = self
- change.version.map(_ => {
- assignments.await { global_state.peek().is_assigned(previous.get_finished) }
- this_actor ! change })
-
+ case Edit_Node(thy_name, header, text_edits) if prover.isDefined =>
+ edit_version(List((thy_name, Some(text_edits))))
reply(())
- case change: Document.Change if prover != null => handle_change(change)
+ case Init_Node(thy_name, header, text) if prover.isDefined =>
+ // FIXME compare with existing node
+ edit_version(List(
+ (thy_name, None),
+ (thy_name, Some(List(Text.Edit.insert(0, text))))))
+ reply(())
+
+ case change: Document.Change if prover.isDefined =>
+ handle_change(change)
case result: Isabelle_Process.Result => handle_result(result)
- case Start(timeout, args) if prover == null =>
+ case Start(timeout, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
- prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
+ prover =
+ Some(new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document)
}
case Stop =>
if (phase == Session.Ready) {
global_state.change(_ => Document.State.init) // FIXME event bus!?
phase = Session.Shutdown
- prover.terminate
+ prover.get.terminate
phase = Session.Inactive
}
finished = true
reply(())
- case bad if prover != null =>
+ case bad if prover.isDefined =>
System.err.println("session_actor: ignoring bad message " + bad)
}
}
@@ -297,7 +350,15 @@
def interrupt() { session_actor ! Interrupt_Prover }
- def edit_version(edits: List[Document.Edit_Text]) { session_actor !? Edit_Version(edits) }
+ def edit_node(thy_name: String, header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
+ {
+ session_actor !? Edit_Node(thy_name, header, edits)
+ }
+
+ def init_node(thy_name: String, header: Exn.Result[Thy_Header.Header], text: String)
+ {
+ session_actor !? Init_Node(thy_name, header, text)
+ }
def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
global_state.peek().snapshot(name, pending_edits)
--- a/src/Pure/Thy/thy_header.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Jul 04 16:54:58 2011 +0200
@@ -9,7 +9,7 @@
import scala.annotation.tailrec
import scala.collection.mutable
-import scala.util.parsing.input.Reader
+import scala.util.parsing.input.{Reader, CharSequenceReader}
import scala.util.matching.Regex
import java.io.File
@@ -36,8 +36,10 @@
/* file name */
- val Thy_Path1 = new Regex("([^/]*)\\.thy")
- val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
+ def thy_path(name: String): Path = Path.basic(name).ext("thy")
+
+ private val Thy_Path1 = new Regex("([^/]*)\\.thy")
+ private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
def split_thy_path(path: String): Option[(String, String)] =
path match {
@@ -99,10 +101,24 @@
}
}
+ def read(source: CharSequence): Header =
+ read(new CharSequenceReader(source))
+
def read(file: File): Header =
{
val reader = Scan.byte_reader(file)
try { read(reader).decode_permissive_utf8 }
finally { reader.close }
}
+
+
+ /* check */
+
+ def check(name: String, source: CharSequence): Header =
+ {
+ val header = read(source)
+ val name1 = header.name
+ if (name == name1) header
+ else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + quote(name1))
+ }
}
--- a/src/Pure/Thy/thy_info.ML Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML Mon Jul 04 16:54:58 2011 +0200
@@ -34,10 +34,11 @@
datatype action = Update | Remove;
local
- val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
+ val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action -> string -> unit) list);
in
- fun add_hook f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change hooks (cons f));
- fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
+ fun add_hook f = Synchronized.change hooks (cons f);
+ fun perform action name =
+ List.app (fn f => (try (fn () => f action name) (); ())) (Synchronized.value hooks);
end;
@@ -135,7 +136,7 @@
(** thy operations **)
-(* remove theory *)
+(* main loader actions *)
fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
if is_finished name then error (loader_msg "attempt to change finished theory" [name])
@@ -151,11 +152,23 @@
if known_thy name then remove_thy name
else ());
+fun update_thy deps theory = NAMED_CRITICAL "Thy_Info" (fn () =>
+ let
+ val name = Context.theory_name theory;
+ val parents = map Context.theory_name (Theory.parents_of theory);
+ val _ = kill_thy name;
+ val _ = map get_theory parents;
+ val _ = change_thys (new_entry name parents (SOME deps, SOME theory));
+ val _ = perform Update name;
+ in () end);
+
(* scheduling loader tasks *)
+type result = theory * unit future * (unit -> unit);
+
datatype task =
- Task of string list * (theory list -> (theory * unit future * (unit -> unit))) |
+ Task of string list * (theory list -> result) |
Finished of theory;
fun task_finished (Task _) = false
@@ -163,15 +176,15 @@
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 (thy, present, commit) = body (map (the o Symtab.lookup tab) parents);
- val _ = Future.join present;
- val _ = commit ();
- in Symtab.update (name, thy) tab end
+ 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 () =>
@@ -199,10 +212,8 @@
val _ =
tasks |> maps (fn name =>
let
- val (thy, present, commit) = Future.join (the (Symtab.lookup futures name));
- val _ = Global_Theory.join_proofs thy;
- val _ = Future.join present;
- val _ = commit ();
+ 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) ();
@@ -226,7 +237,7 @@
fun required_by _ [] = ""
| required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-fun load_thy initiators update_time (deps: deps) text name parent_thys =
+fun load_thy initiators update_time deps text name parent_thys =
let
val _ = kill_thy name;
val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
@@ -240,13 +251,7 @@
|> Present.begin_theory update_time dir uses;
val (theory, present) = Outer_Syntax.load_thy name init pos text;
-
- val parents = map Context.theory_name parent_thys;
- fun commit () =
- NAMED_CRITICAL "Thy_Info" (fn () =>
- (map get_theory parents;
- change_thys (new_entry name parents (SOME deps, SOME theory));
- perform Update name));
+ fun commit () = update_thy deps theory;
in (theory, present, commit) end;
fun check_deps dir name =
@@ -274,13 +279,14 @@
let
val path = Path.expand (Path.explode str);
val name = Path.implode (Path.base path);
- val dir' = Path.append dir (Path.dir path);
- val _ = member (op =) initiators name andalso error (cycle_msg initiators);
in
(case try (Graph.get_node tasks) name of
SOME task => (task_finished task, tasks)
| NONE =>
let
+ val dir' = Path.append dir (Path.dir path);
+ val _ = member (op =) initiators name andalso error (cycle_msg initiators);
+
val (current, deps, imports) = check_deps dir' name
handle ERROR msg => cat_error msg
(loader_msg "the error(s) above occurred while examining theory" [name] ^
@@ -332,16 +338,12 @@
let
val name = Context.theory_name theory;
val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
- val parents = map Context.theory_name (Theory.parents_of theory);
val imports = Thy_Load.imports_of theory;
- val deps = make_deps master imports;
in
NAMED_CRITICAL "Thy_Info" (fn () =>
(kill_thy name;
Output.urgent_message ("Registering theory " ^ quote name);
- map get_theory parents;
- change_thys (new_entry name parents (SOME deps, SOME theory));
- perform Update name))
+ update_thy (make_deps master imports) theory))
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_info.scala Mon Jul 04 16:54:58 2011 +0200
@@ -0,0 +1,59 @@
+/* Title: Pure/Thy/thy_info.scala
+ Author: Makarius
+
+Theory and file dependencies.
+*/
+
+package isabelle
+
+
+class Thy_Info(thy_load: Thy_Load)
+{
+ /* messages */
+
+ private def show_path(names: List[String]): String =
+ names.map(quote).mkString(" via ")
+
+ private def cycle_msg(names: List[String]): String =
+ "Cyclic dependency of " + show_path(names)
+
+ private def required_by(s: String, initiators: List[String]): String =
+ if (initiators.isEmpty) ""
+ else s + "(required by " + show_path(initiators.reverse) + ")"
+
+
+ /* dependencies */
+
+ type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header)
+
+ private def require_thys(
+ initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
+ (deps /: strs)(require_thy(initiators, dir, _, _))
+
+ private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
+ {
+ val path = Path.explode(str)
+ val name = path.base.implode
+
+ if (deps.isDefinedAt(name)) deps
+ else {
+ val dir1 = dir + path.dir
+ try {
+ if (initiators.contains(name)) error(cycle_msg(initiators))
+ val (text, header) =
+ try { thy_load.check_thy(dir1, name) }
+ catch {
+ case ERROR(msg) =>
+ cat_error(msg, "The error(s) above occurred while examining theory " +
+ quote(name) + required_by("\n", initiators))
+ }
+ require_thys(name :: initiators, dir1,
+ deps + (name -> Exn.Res(text, header)), header.imports)
+ }
+ catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
+ }
+ }
+
+ def dependencies(dir: Path, str: String): Deps =
+ require_thy(Nil, dir, Map.empty, str) // FIXME capture errors in str (!??)
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_load.scala Mon Jul 04 16:54:58 2011 +0200
@@ -0,0 +1,13 @@
+/* Title: Pure/Thy/thy_load.scala
+ Author: Makarius
+
+Loading files that contribute to a theory.
+*/
+
+package isabelle
+
+abstract class Thy_Load
+{
+ def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
+}
+
--- a/src/Pure/Thy/thy_syntax.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Jul 04 16:54:58 2011 +0200
@@ -99,7 +99,7 @@
/** text edits **/
- def text_edits(session: Session, previous: Document.Version,
+ def text_edits(syntax: Outer_Syntax, new_id: () => Document.ID, previous: Document.Version,
edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
{
/* phase 1: edit individual command source */
@@ -147,7 +147,7 @@
commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
val sources = range.flatMap(_.span.map(_.source))
- val spans0 = parse_spans(session.current_syntax().scan(sources.mkString))
+ val spans0 = parse_spans(syntax.scan(sources.mkString))
val (before_edit, spans1) =
if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
@@ -159,7 +159,7 @@
(Some(last), spans1.take(spans1.length - 1))
else (commands.next(last), spans1)
- val inserted = spans2.map(span => new Command(session.new_id(), span))
+ val inserted = spans2.map(span => new Command(new_id(), span))
val new_commands =
commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
recover_spans(new_commands)
@@ -195,7 +195,7 @@
doc_edits += (name -> Some(cmd_edits))
nodes += (name -> new Document.Node(commands2))
}
- (doc_edits.toList, new Document.Version(session.new_id(), nodes))
+ (doc_edits.toList, new Document.Version(new_id(), nodes))
}
}
}
--- a/src/Pure/build-jars Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/build-jars Mon Jul 04 16:54:58 2011 +0200
@@ -50,6 +50,8 @@
Thy/completion.scala
Thy/html.scala
Thy/thy_header.scala
+ Thy/thy_info.scala
+ Thy/thy_load.scala
Thy/thy_syntax.scala
library.scala
package.scala
--- a/src/Pure/library.ML Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/library.ML Mon Jul 04 16:54:58 2011 +0200
@@ -28,7 +28,7 @@
val funpow: int -> ('a -> 'a) -> 'a -> 'a
val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
- (*errors*)
+ (*user errors*)
exception ERROR of string
val error: string -> 'a
val cat_error: string -> string -> 'a
@@ -260,7 +260,7 @@
| funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
-(* errors *)
+(* user errors *)
exception ERROR of string;
fun error msg = raise ERROR msg;
--- a/src/Pure/library.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/library.scala Mon Jul 04 16:54:58 2011 +0200
@@ -18,6 +18,27 @@
object Library
{
+ /* user errors */
+
+ object ERROR
+ {
+ def apply(message: String): Throwable = new RuntimeException(message)
+ def unapply(exn: Throwable): Option[String] =
+ exn match {
+ case e: RuntimeException =>
+ val msg = e.getMessage
+ Some(if (msg == null) "" else msg)
+ case _ => None
+ }
+ }
+
+ def error(message: String): Nothing = throw ERROR(message)
+
+ def cat_error(msg1: String, msg2: String): Nothing =
+ if (msg1 == "") error(msg1)
+ else error(msg1 + "\n" + msg2)
+
+
/* lists */
def separate[A](s: A, list: List[A]): List[A] =
@@ -41,6 +62,37 @@
}
+ /* iterate over chunks (cf. space_explode) */
+
+ def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
+ {
+ private val end = source.length
+ private def next_chunk(i: Int): Option[(CharSequence, Int)] =
+ {
+ if (i < end) {
+ var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
+ Some((source.subSequence(i + 1, j), j))
+ }
+ else None
+ }
+ private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
+
+ def hasNext(): Boolean = state.isDefined
+ def next(): CharSequence =
+ state match {
+ case Some((s, i)) => { state = next_chunk(i); s }
+ case None => Iterator.empty.next()
+ }
+ }
+
+ def first_line(source: CharSequence): String =
+ {
+ val lines = chunks(source)
+ if (lines.hasNext) lines.next.toString
+ else ""
+ }
+
+
/* strings */
def quote(s: String): String = "\"" + s + "\""
@@ -73,37 +125,6 @@
}
- /* iterate over chunks (cf. space_explode/split_lines in ML) */
-
- def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
- {
- private val end = source.length
- private def next_chunk(i: Int): Option[(CharSequence, Int)] =
- {
- if (i < end) {
- var j = i; do j += 1 while (j < end && source.charAt(j) != sep)
- Some((source.subSequence(i + 1, j), j))
- }
- else None
- }
- private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1)
-
- def hasNext(): Boolean = state.isDefined
- def next(): CharSequence =
- state match {
- case Some((s, i)) => { state = next_chunk(i); s }
- case None => Iterator.empty.next()
- }
- }
-
- def first_line(source: CharSequence): String =
- {
- val lines = chunks(source)
- if (lines.hasNext) lines.next.toString
- else ""
- }
-
-
/* simple dialogs */
private def simple_dialog(kind: Int, default_title: String)
@@ -160,3 +181,17 @@
Exn.release(result)
}
}
+
+
+class Basic_Library
+{
+ val space_explode = Library.space_explode _
+
+ val quote = Library.quote _
+ val commas = Library.commas _
+ val commas_quote = Library.commas_quote _
+
+ val ERROR = Library.ERROR
+ val error = Library.error _
+ val cat_error = Library.cat_error _
+}
--- a/src/Pure/package.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Pure/package.scala Mon Jul 04 16:54:58 2011 +0200
@@ -4,8 +4,7 @@
Toplevel isabelle package.
*/
-package object isabelle
+package object isabelle extends isabelle.Basic_Library
{
- def error(message: String): Nothing = throw new RuntimeException(message)
}
--- a/src/Tools/jEdit/src/document_model.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Mon Jul 04 16:54:58 2011 +0200
@@ -45,10 +45,10 @@
}
}
- def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
+ def init(session: Session, buffer: Buffer, master_dir: String, thy_name: String): Document_Model =
{
exit(buffer)
- val model = new Document_Model(session, buffer, thy_name)
+ val model = new Document_Model(session, buffer, master_dir, thy_name)
buffer.setProperty(key, model)
model.activate()
model
@@ -56,31 +56,36 @@
}
-class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
+class Document_Model(val session: Session,
+ val buffer: Buffer, val master_dir: String, val thy_name: String)
{
/* pending text edits */
- object pending_edits // owned by Swing thread
+ private def capture_header(): Exn.Result[Thy_Header.Header] =
+ Exn.capture {
+ session.thy_header.check(thy_name, buffer.getSegment(0, buffer.getLength))
+ }
+
+ private object pending_edits // owned by Swing thread
{
private val pending = new mutable.ListBuffer[Text.Edit]
def snapshot(): List[Text.Edit] = pending.toList
- def flush(more_edits: Option[List[Text.Edit]]*)
+ def flush()
{
Swing_Thread.require()
- val edits = snapshot()
- pending.clear
-
- val all_edits =
- if (edits.isEmpty) more_edits.toList
- else Some(edits) :: more_edits.toList
- if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
+ snapshot() match {
+ case Nil =>
+ case edits =>
+ pending.clear
+ session.edit_node(master_dir + "/" + thy_name, capture_header(), edits)
+ }
}
def init()
{
- Swing_Thread.require()
- flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
+ flush()
+ session.init_node(master_dir + "/" + thy_name, capture_header(), Isabelle.buffer_text(buffer))
}
private val delay_flush =
@@ -100,7 +105,7 @@
def snapshot(): Document.Snapshot =
{
Swing_Thread.require()
- session.snapshot(thy_name, pending_edits.snapshot())
+ session.snapshot(master_dir + "/" + thy_name, pending_edits.snapshot())
}
--- a/src/Tools/jEdit/src/document_view.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Mon Jul 04 16:54:58 2011 +0200
@@ -78,7 +78,7 @@
Swing_Thread.require()
if (model.buffer == text_area.getBuffer) body
else {
- Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
+ Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
default
}
}
--- a/src/Tools/jEdit/src/plugin.scala Mon Jul 04 10:23:46 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Mon Jul 04 16:54:58 2011 +0200
@@ -10,14 +10,14 @@
import isabelle._
import java.lang.System
-import java.io.{FileInputStream, IOException}
+import java.io.{File, FileInputStream, IOException}
import java.awt.Font
import scala.collection.mutable
import scala.swing.ComboBox
import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
- Buffer, EditPane, ServiceManager, View}
+ Buffer, EditPane, MiscUtilities, ServiceManager, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
@@ -201,8 +201,8 @@
case None =>
// FIXME strip protocol prefix of URL
Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
- case Some((dir, thy_name)) =>
- Some(Document_Model.init(session, buffer, dir + "/" + thy_name))
+ case Some((master_dir, thy_name)) =>
+ Some(Document_Model.init(session, buffer, master_dir, thy_name))
case None => None
}
}
@@ -314,15 +314,30 @@
class Plugin extends EBPlugin
{
- /* session management */
+ /* editor file store */
+
+ private val file_store = new Session.File_Store
+ {
+ def read(path: Path): String =
+ {
+ val platform_path = Isabelle.system.platform_path(path)
+ val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
- @volatile private var session_ready = false
+ 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))
+ }
+ }
+ }
+
+
+ /* session manager */
private val session_manager = actor {
loop {
react {
case phase: Session.Phase =>
- session_ready = phase == Session.Ready
phase match {
case Session.Failed =>
Swing_Thread.now {
@@ -335,7 +350,6 @@
case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
case _ =>
}
-
case bad => System.err.println("session_manager: ignoring bad message " + bad)
}
}
@@ -357,7 +371,7 @@
if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
val buffer = msg.getBuffer
- if (buffer != null && session_ready)
+ if (buffer != null && Isabelle.session.is_ready)
Isabelle.init_model(buffer)
case msg: EditPaneUpdate
@@ -373,7 +387,7 @@
if (buffer != null && text_area != null) {
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
msg.getWhat == EditPaneUpdate.CREATED) {
- if (session_ready)
+ if (Isabelle.session.is_ready)
Isabelle.init_view(buffer, text_area)
}
else Isabelle.exit_view(buffer, text_area)
@@ -393,7 +407,7 @@
Isabelle.setup_tooltips()
Isabelle.system = new Isabelle_System
Isabelle.system.install_fonts()
- Isabelle.session = new Session(Isabelle.system)
+ Isabelle.session = new Session(Isabelle.system, file_store)
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
if (ModeProvider.instance.isInstanceOf[ModeProvider])
ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)