--- a/lib/scripts/getsettings Thu Mar 01 11:28:56 2012 +0100
+++ b/lib/scripts/getsettings Thu Mar 01 14:48:32 2012 +0100
@@ -55,8 +55,8 @@
#JVM path wrapper
if [ "$OSTYPE" = cygwin ]; then
- CLASSPATH="$(cygpath -u -p "$CLASSPATH")"
- function jvmpath() { cygpath -C UTF8 -w -p "$@"; }
+ CLASSPATH="$(cygpath -i -u -p "$CLASSPATH")"
+ function jvmpath() { cygpath -i -C UTF8 -w -p "$@"; }
THIS_CYGWIN="$(jvmpath "/")"
else
function jvmpath() { echo "$@"; }
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Thu Mar 01 11:28:56 2012 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Thu Mar 01 14:48:32 2012 +0100
@@ -28,8 +28,8 @@
"list_all' P xs \<equiv> list_all'_rec P 0 xs"
lemma list_all'_rec:
- "\<And>n. list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
- apply (induct xs)
+ "list_all'_rec P n xs = (\<forall>p < size xs. P (xs!p) (p+n))"
+ apply (induct xs arbitrary: n)
apply auto
apply (case_tac p)
apply auto
--- a/src/HOL/MicroJava/Comp/Index.thy Thu Mar 01 11:28:56 2012 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy Thu Mar 01 14:48:32 2012 +0100
@@ -127,7 +127,7 @@
lemma wf_java_mdecl_disjoint_varnames:
"wf_java_mdecl G C (S,rT,(pns,lvars,blk,res))
\<Longrightarrow> disjoint_varnames pns lvars"
-apply (case_tac S)
+apply (cases S)
apply (simp add: wf_java_mdecl_def disjoint_varnames_def map_of_in_set)
done
--- a/src/Pure/PIDE/document.ML Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/PIDE/document.ML Thu Mar 01 14:48:32 2012 +0100
@@ -212,15 +212,15 @@
|> touch_node name
| Header header =>
let
- val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
+ val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []);
val nodes1 = nodes
|> default_node name
- |> fold default_node parents;
+ |> fold default_node imports;
val nodes2 = nodes1
|> Graph.Keys.fold
(fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
val (header', nodes3) =
- (header, Graph.add_deps_acyclic (name, parents) nodes2)
+ (header, Graph.add_deps_acyclic (name, imports) nodes2)
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
in Graph.map_node name (set_header header') nodes3 end
|> touch_node name
--- a/src/Pure/PIDE/document.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/PIDE/document.scala Thu Mar 01 14:48:32 2012 +0100
@@ -35,10 +35,12 @@
type Edit_Text = Edit[Text.Edit, Text.Perspective]
type Edit_Command = Edit[(Option[Command], Option[Command]), Command.Perspective]
- type Node_Header = Exn.Result[Thy_Header]
+ type Node_Header = Exn.Result[Node.Deps]
object Node
{
+ sealed case class Deps(imports: List[Name], uses: List[(String, Boolean)])
+
object Name
{
val empty = Name("", "", "")
@@ -81,12 +83,6 @@
case class Header[A, B](header: Node_Header) extends Edit[A, B]
case class Perspective[A, B](perspective: B) extends Edit[A, B]
- def norm_header(f: String => String, g: String => String, header: Node_Header): Node_Header =
- header match {
- case Exn.Res(h) => Exn.capture { h.norm_deps(f, g) }
- case exn => exn
- }
-
def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
: Iterator[(Command, Text.Offset)] =
{
@@ -192,17 +188,15 @@
def + (entry: (Node.Name, Node)): Nodes =
{
val (name, node) = entry
- val parents =
+ val imports =
node.header match {
- case Exn.Res(header) =>
- // FIXME official names of yet unknown nodes!?
- for (imp <- header.imports; imp_name <- get_name(imp)) yield imp_name
+ case Exn.Res(deps) => deps.imports
case _ => Nil
}
val graph1 =
- (graph.default_node(name, Node.empty) /: parents)((g, p) => g.default_node(p, Node.empty))
+ (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
- val graph3 = (graph2 /: parents)((g, dep) => g.add_edge(dep, name))
+ val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
new Nodes(graph3.map_node(name, _ => node))
}
--- a/src/Pure/PIDE/protocol.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala Thu Mar 01 14:48:32 2012 +0100
@@ -211,22 +211,24 @@
val edits_yxml =
{ import XML.Encode._
def id: T[Command] = (cmd => long(cmd.id))
- def encode_edit(dir: String)
+ def encode_edit(name: Document.Node.Name)
: T[Document.Node.Edit[(Option[Command], Option[Command]), Command.Perspective]] =
variant(List(
{ case Document.Node.Clear() => (Nil, Nil) },
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
- { case Document.Node.Header(Exn.Res(Thy_Header(a, b, c))) =>
+ { case Document.Node.Header(Exn.Res(deps)) =>
+ val dir = Isabelle_System.posix_path(name.dir)
+ val imports = deps.imports.map(_.node)
+ val uses = deps.uses.map(p => (Isabelle_System.posix_path(p._1), p._2))
(Nil,
triple(pair(string, string), list(string), list(pair(string, bool)))(
- (dir, a), b, c)) },
+ (dir, name.theory), imports, uses)) },
{ case Document.Node.Header(Exn.Exn(e)) => (List(Exn.message(e)), Nil) },
{ case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
def encode: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
{
val (name, edit) = node_edit
- val dir = Isabelle_System.posix_path(name.dir)
- pair(string, encode_edit(dir))(name.node, edit)
+ pair(string, encode_edit(name))(name.node, edit)
})
YXML.string_of_body(encode(edits)) }
input("Document.update", Document.ID(old_id), Document.ID(new_id), edits_yxml)
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Mar 01 14:48:32 2012 +0100
@@ -143,7 +143,7 @@
Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
handle ERROR msg =>
(warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
- tell_file_retracted (Thy_Header.thy_path name))
+ tell_file_retracted (Thy_Load.thy_path (Path.basic name)))
val _ = Isar.init ();
in () end;
--- a/src/Pure/System/session.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/System/session.scala Thu Mar 01 14:48:32 2012 +0100
@@ -143,20 +143,11 @@
def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
{
- def norm_import(s: String): String =
- {
- val thy_name = Thy_Header.base_name(s)
- if (thy_load.is_loaded(thy_name)) thy_name
- else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
- }
- def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
-
val header1: Document.Node_Header =
header match {
- case Exn.Res(Thy_Header(thy_name, _, _))
- if (thy_load.is_loaded(thy_name)) =>
- Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
- case _ => Document.Node.norm_header(norm_import, norm_use, header)
+ case Exn.Res(_) if (thy_load.is_loaded(name.theory)) =>
+ Exn.Exn(ERROR("Attempt to update loaded theory " + quote(name.theory)))
+ case _ => header
}
(name, Document.Node.Header(header1))
}
--- a/src/Pure/System/swing_thread.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/System/swing_thread.scala Thu Mar 01 14:48:32 2012 +0100
@@ -45,7 +45,7 @@
/* delayed actions */
- private def delayed_action(first: Boolean)(time: Time)(action: => Unit): () => Unit =
+ private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Boolean => Unit =
{
val listener = new ActionListener {
override def actionPerformed(e: ActionEvent) { Swing_Thread.assert(); action }
@@ -54,7 +54,9 @@
timer.setRepeats(false)
def invoke() { later { if (first) timer.start() else timer.restart() } }
- invoke _
+ def revoke() { timer.stop() }
+
+ (active: Boolean) => if (active) invoke() else revoke()
}
// delayed action after first invocation
--- a/src/Pure/Thy/thy_header.ML Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML Thu Mar 01 14:48:32 2012 +0100
@@ -8,8 +8,6 @@
sig
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 consistent_name: string -> string -> unit
end;
structure Thy_Header: THY_HEADER =
@@ -67,13 +65,4 @@
| NONE => error ("Unexpected end of input" ^ Position.str_of pos))
end;
-
-(* file name *)
-
-val thy_path = Path.ext "thy" o Path.basic;
-
-fun consistent_name name name' =
- if name = name' then ()
- else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
-
end;
--- a/src/Pure/Thy/thy_header.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_header.scala Thu Mar 01 14:48:32 2012 +0100
@@ -37,8 +37,6 @@
def thy_name(s: String): Option[String] =
s match { case Thy_Name(name) => Some(name) case _ => None }
- def thy_path(path: Path): Path = path.ext("thy")
-
/* header */
@@ -96,18 +94,6 @@
try { read(reader).map(Standard_System.decode_permissive_utf8) }
finally { reader.close }
}
-
-
- /* check */
-
- def check(name: String, source: CharSequence): Thy_Header =
- {
- val header = read(source)
- val name1 = header.name
- val path = Path.explode(name)
- if (name != name1) error("Bad file name " + thy_path(path) + " for theory " + quote(name1))
- header
- }
}
@@ -116,10 +102,5 @@
{
def map(f: String => String): Thy_Header =
Thy_Header(f(name), imports.map(f), uses.map(p => (f(p._1), p._2)))
-
- def norm_deps(f: String => String, g: String => String): Thy_Header =
- copy(imports = imports.map(name => f(name)))
- // FIXME
- // copy(imports = imports.map(name => f(name)), uses = uses.map(p => (g(p._1), p._2)))
}
--- a/src/Pure/Thy/thy_info.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_info.scala Thu Mar 01 14:48:32 2012 +0100
@@ -24,15 +24,6 @@
/* dependencies */
- def import_name(dir: String, str: String): Document.Node.Name =
- {
- val path = Path.explode(str)
- val node = thy_load.append(dir, Thy_Header.thy_path(path))
- val dir1 = thy_load.append(dir, path.dir)
- val theory = path.base.implode
- Document.Node.Name(node, dir1, theory)
- }
-
type Dep = (Document.Node.Name, Document.Node_Header)
private type Required = (List[Dep], Set[Document.Node.Name])
@@ -49,16 +40,16 @@
else {
try {
if (initiators.contains(name)) error(cycle_msg(initiators))
- val header =
+ val node_deps =
try { thy_load.check_thy(name) }
catch {
case ERROR(msg) =>
cat_error(msg, "The error(s) above occurred while examining theory " +
quote(name.theory) + required_by(initiators))
}
- val imports = header.imports.map(import_name(name.dir, _))
- val (deps1, seen1) = require_thys(name :: initiators, (deps, seen + name), imports)
- ((name, Exn.Res(header)) :: deps1, seen1)
+ val (deps1, seen1) =
+ require_thys(name :: initiators, (deps, seen + name), node_deps.imports)
+ ((name, Exn.Res(node_deps)) :: deps1, seen1)
}
catch { case e: Throwable => (((name, Exn.Exn(e)): Dep) :: deps, seen + name) }
}
--- a/src/Pure/Thy/thy_load.ML Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_load.ML Thu Mar 01 14:48:32 2012 +0100
@@ -10,6 +10,7 @@
val imports_of: theory -> string list
val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
val check_file: Path.T -> Path.T -> Path.T
+ val thy_path: Path.T -> Path.T
val check_thy: Path.T -> string ->
{master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list}
val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
@@ -75,14 +76,18 @@
fun check_file dir file = File.check_file (File.full_path dir file);
+val thy_path = Path.ext "thy";
+
fun check_thy dir name =
let
- val master_file = check_file dir (Thy_Header.thy_path name);
+ val path = thy_path (Path.basic name);
+ val master_file = check_file dir path;
val text = File.read master_file;
val (name', imports, uses) =
if name = Context.PureN then (Context.PureN, [], [])
else Thy_Header.read (Path.position master_file) text;
- val _ = Thy_Header.consistent_name name name';
+ val _ = name <> name' andalso
+ error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name');
in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
--- a/src/Pure/Thy/thy_load.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_load.scala Thu Mar 01 14:48:32 2012 +0100
@@ -29,11 +29,39 @@
def append(dir: String, source_path: Path): String =
(Path.explode(dir) + source_path).implode
- def check_thy(name: Document.Node.Name): Thy_Header =
+ def read_header(name: Document.Node.Name): Thy_Header =
{
val file = new File(name.node)
if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
Thy_Header.read(file)
}
+
+
+ /* theory files */
+
+ def thy_path(path: Path): Path = path.ext("thy")
+
+ private def import_name(dir: String, s: String): Document.Node.Name =
+ {
+ val theory = Thy_Header.base_name(s)
+ if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
+ else {
+ val path = Path.explode(s)
+ val node = append(dir, thy_path(path))
+ val dir1 = append(dir, path.dir)
+ Document.Node.Name(node, dir1, theory)
+ }
+ }
+
+ def check_thy(name: Document.Node.Name): Document.Node.Deps =
+ {
+ val header = read_header(name)
+ val name1 = header.name
+ val imports = header.imports.map(import_name(name.dir, _))
+ val uses = header.uses.map(p => (append(name.dir, Path.explode(p._1)), p._2))
+ if (name.theory != name1)
+ error("Bad file name " + thy_path(Path.basic(name.theory)) + " for theory " + quote(name1))
+ Document.Node.Deps(imports, uses)
+ }
}
--- a/src/Pure/Thy/thy_syntax.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Thu Mar 01 14:48:32 2012 +0100
@@ -258,7 +258,7 @@
val node = nodes(name)
val update_header =
(node.header, header) match {
- case (Exn.Res(thy_header0), Exn.Res(thy_header)) => thy_header0 != thy_header
+ case (Exn.Res(deps0), Exn.Res(deps)) => deps != deps
case _ => true
}
if (update_header) {
--- a/src/Tools/Code/code_runtime.ML Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/Code/code_runtime.ML Thu Mar 01 14:48:32 2012 +0100
@@ -310,8 +310,9 @@
| process_reflection (code, _) _ (SOME file_name) thy =
let
val preamble =
- "(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy))
- ^ "; DO NOT EDIT! *)";
+ "(* Generated from " ^
+ Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^
+ "; DO NOT EDIT! *)";
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
in
thy
--- a/src/Tools/jEdit/src/document_model.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Thu Mar 01 14:48:32 2012 +0100
@@ -60,10 +60,12 @@
{
/* header */
- def node_header(): Exn.Result[Thy_Header] =
+ def node_header(): Document.Node_Header =
{
Swing_Thread.require()
- Exn.capture { Thy_Header.check(name.theory, buffer.getSegment(0, buffer.getLength)) }
+ if (Isabelle.jedit_buffer(name.node) == Some(buffer))
+ Exn.capture { Isabelle.thy_load.check_thy(name) }
+ else Exn.Exn(ERROR("Bad theory header")) // FIXME odd race condition!?
}
@@ -109,12 +111,6 @@
}
}
- def init()
- {
- flush()
- session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
- }
-
private val delay_flush =
Swing_Thread.delay_last(session.input_delay) { flush() }
@@ -122,13 +118,25 @@
{
Swing_Thread.require()
pending += edit
- delay_flush()
+ delay_flush(true)
}
def update_perspective()
{
pending_perspective = true
- delay_flush()
+ delay_flush(true)
+ }
+
+ def init()
+ {
+ flush()
+ session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
+ }
+
+ def exit()
+ {
+ delay_flush(false)
+ flush()
}
}
@@ -190,7 +198,7 @@
private def deactivate()
{
- pending_edits.flush()
+ pending_edits.exit()
buffer.removeBufferListener(buffer_listener)
Token_Markup.refresh_buffer(buffer)
}
--- a/src/Tools/jEdit/src/document_view.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Thu Mar 01 14:48:32 2012 +0100
@@ -343,11 +343,13 @@
update_snapshot().node.proper_command_at(text_area.getCaretPosition)
}
- private val caret_listener = new CaretListener {
- private val delay = Swing_Thread.delay_last(session.input_delay) {
+ private val delay_caret_update =
+ Swing_Thread.delay_last(session.input_delay) {
session.caret_focus.event(Session.Caret_Focus)
}
- override def caretUpdate(e: CaretEvent) { delay() }
+
+ private val caret_listener = new CaretListener {
+ override def caretUpdate(e: CaretEvent) { delay_caret_update(true) }
}
@@ -373,7 +375,7 @@
if (updated ||
(changed.nodes.contains(model.name) &&
changed.commands.exists(snapshot.node.commands.contains)))
- overview.delay_repaint()
+ overview.delay_repaint(true)
visible_range() match {
case None =>
@@ -430,8 +432,8 @@
text_area.removeFocusListener(focus_listener)
text_area.getView.removeWindowListener(window_listener)
painter.removeMouseMotionListener(mouse_motion_listener)
- text_area.removeCaretListener(caret_listener)
- text_area.removeLeftOfScrollBar(overview)
+ text_area.removeCaretListener(caret_listener); delay_caret_update(false)
+ text_area.removeLeftOfScrollBar(overview); overview.delay_repaint(false)
text_area.getGutter.removeExtension(gutter_painter)
text_area_painter.deactivate()
painter.removeExtension(tooltip_painter)
--- a/src/Tools/jEdit/src/jedit_thy_load.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Thu Mar 01 14:48:32 2012 +0100
@@ -52,7 +52,7 @@
}
}
- override def check_thy(name: Document.Node.Name): Thy_Header =
+ override def read_header(name: Document.Node.Name): Thy_Header =
{
Swing_Thread.now {
Isabelle.jedit_buffer(name.node) match {
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Mar 01 14:48:32 2012 +0100
@@ -126,14 +126,17 @@
Isabelle.session.global_settings -= main_actor
Isabelle.session.commands_changed -= main_actor
Isabelle.session.caret_focus -= main_actor
+ delay_resize(false)
}
/* resize */
+ private val delay_resize =
+ Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
+
addComponentListener(new ComponentAdapter {
- val delay = Swing_Thread.delay_first(Isabelle.session.update_delay) { handle_resize() }
- override def componentResized(e: ComponentEvent) { delay() }
+ override def componentResized(e: ComponentEvent) { delay_resize(true) }
})
--- a/src/Tools/jEdit/src/plugin.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Mar 01 14:48:32 2012 +0100
@@ -390,9 +390,12 @@
case Session.Ready =>
Isabelle.jedit_buffers.foreach(Isabelle.init_model)
- delay_load()
+ delay_load(true)
- case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+ case Session.Shutdown =>
+ Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+ delay_load(false)
+
case _ =>
}
case bad => System.err.println("session_manager: ignoring bad message " + bad)
@@ -416,7 +419,7 @@
if (Isabelle.session.is_ready) {
val buffer = msg.getBuffer
if (buffer != null) Isabelle.init_model(buffer)
- delay_load()
+ delay_load(true)
}
case msg: EditPaneUpdate
--- a/src/Tools/jEdit/src/session_dockable.scala Thu Mar 01 11:28:56 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala Thu Mar 01 14:48:32 2012 +0100
@@ -155,7 +155,8 @@
}
val nodes_status1 =
(nodes_status /: iterator)({ case (status, (name, node)) =>
- status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
+ if (Isabelle.thy_load.is_loaded(name.theory)) status
+ else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
if (nodes_status != nodes_status1) {
nodes_status = nodes_status1