1.1 --- a/src/Pure/General/path.scala Mon Jul 04 10:23:46 2011 +0200
1.2 +++ b/src/Pure/General/path.scala Mon Jul 04 16:54:58 2011 +0200
1.3 @@ -19,7 +19,7 @@
1.4 private case object Parent extends Elem
1.5
1.6 private def err_elem(msg: String, s: String): Nothing =
1.7 - error (msg + " path element specification: " + Library.quote(s))
1.8 + error (msg + " path element specification: " + quote(s))
1.9
1.10 private def check_elem(s: String): String =
1.11 if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
1.12 @@ -27,7 +27,7 @@
1.13 s.iterator.filter(c => c == '/' || c == '\\' || c == '$' || c == ':').toList match {
1.14 case Nil => s
1.15 case bads =>
1.16 - err_elem ("Illegal character(s) " + Library.commas_quote(bads.map(_.toString)) + " in", s)
1.17 + err_elem ("Illegal character(s) " + commas_quote(bads.map(_.toString)) + " in", s)
1.18 }
1.19
1.20 private def root_elem(s: String): Elem = Root(check_elem(s))
1.21 @@ -114,7 +114,7 @@
1.22 case _ => elems.map(Path.implode_elem).reverse.mkString("/")
1.23 }
1.24
1.25 - override def toString: String = Library.quote(implode)
1.26 + override def toString: String = quote(implode)
1.27
1.28
1.29 /* base element */
2.1 --- a/src/Pure/General/yxml.scala Mon Jul 04 10:23:46 2011 +0200
2.2 +++ b/src/Pure/General/yxml.scala Mon Jul 04 16:54:58 2011 +0200
2.3 @@ -144,12 +144,12 @@
2.4 def parse_body_failsafe(source: CharSequence): XML.Body =
2.5 {
2.6 try { parse_body(source) }
2.7 - catch { case _: RuntimeException => List(markup_failsafe(source)) }
2.8 + catch { case ERROR(_) => List(markup_failsafe(source)) }
2.9 }
2.10
2.11 def parse_failsafe(source: CharSequence): XML.Tree =
2.12 {
2.13 try { parse(source) }
2.14 - catch { case _: RuntimeException => markup_failsafe(source) }
2.15 + catch { case ERROR(_) => markup_failsafe(source) }
2.16 }
2.17 }
3.1 --- a/src/Pure/PIDE/document.ML Mon Jul 04 10:23:46 2011 +0200
3.2 +++ b/src/Pure/PIDE/document.ML Mon Jul 04 16:54:58 2011 +0200
3.3 @@ -80,10 +80,10 @@
3.4 NONE => entries
3.5 | SOME next => Entries.update (next, NONE) entries);
3.6
3.7 -fun edit_node (hook, SOME id2) (Node entries) =
3.8 - Node (Entries.insert_after hook (id2, NONE) entries)
3.9 - | edit_node (hook, NONE) (Node entries) =
3.10 - Node (entries |> Entries.delete_after hook |> reset_after hook);
3.11 +fun edit_node (id, SOME id2) (Node entries) =
3.12 + Node (Entries.insert_after id (id2, NONE) entries)
3.13 + | edit_node (id, NONE) (Node entries) =
3.14 + Node (entries |> Entries.delete_after id |> reset_after id);
3.15
3.16
3.17 (* version operations *)
4.1 --- a/src/Pure/PIDE/text.scala Mon Jul 04 10:23:46 2011 +0200
4.2 +++ b/src/Pure/PIDE/text.scala Mon Jul 04 16:54:58 2011 +0200
4.3 @@ -46,7 +46,7 @@
4.4
4.5 def try_restrict(that: Range): Option[Range] =
4.6 try { Some (restrict(that)) }
4.7 - catch { case _: RuntimeException => None }
4.8 + catch { case ERROR(_) => None }
4.9 }
4.10
4.11
4.12 @@ -57,7 +57,7 @@
4.13 def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
4.14 def try_restrict(r: Text.Range): Option[Info[A]] =
4.15 try { Some(Info(range.restrict(r), info)) }
4.16 - catch { case _: RuntimeException => None }
4.17 + catch { case ERROR(_) => None }
4.18 }
4.19
4.20
5.1 --- a/src/Pure/System/cygwin.scala Mon Jul 04 10:23:46 2011 +0200
5.2 +++ b/src/Pure/System/cygwin.scala Mon Jul 04 16:54:58 2011 +0200
5.3 @@ -115,7 +115,7 @@
5.4 try {
5.5 Download.file(parent, "Downloading", new URL("http://www.cygwin.com/setup.exe"), setup_exe)
5.6 }
5.7 - catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
5.8 + catch { case ERROR(_) => error("Failed to download Cygwin setup program") }
5.9
5.10 val (_, rc) = Standard_System.raw_exec(root, null, true,
5.11 setup_exe.toString, "-R", root.toString, "-l", download.toString,
6.1 --- a/src/Pure/System/gui_setup.scala Mon Jul 04 10:23:46 2011 +0200
6.2 +++ b/src/Pure/System/gui_setup.scala Mon Jul 04 16:54:58 2011 +0200
6.3 @@ -51,9 +51,7 @@
6.4 if (platform64 != "") text.append("Isabelle platform (64 bit): " + platform64 + "\n")
6.5 text.append("Isabelle home: " + isabelle_system.getenv("ISABELLE_HOME") + "\n")
6.6 text.append("Isabelle java: " + isabelle_system.this_java() + "\n")
6.7 - } catch {
6.8 - case e: RuntimeException => text.append(e.getMessage + "\n")
6.9 - }
6.10 + } catch { case ERROR(msg) => text.append(msg + "\n") }
6.11
6.12 // reactions
6.13 listenTo(ok)
7.1 --- a/src/Pure/System/session.scala Mon Jul 04 10:23:46 2011 +0200
7.2 +++ b/src/Pure/System/session.scala Mon Jul 04 16:54:58 2011 +0200
7.3 @@ -2,7 +2,7 @@
7.4 Author: Makarius
7.5 Options: :folding=explicit:collapseFolds=1:
7.6
7.7 -Isabelle session, potentially with running prover.
7.8 +Main Isabelle/Scala session, potentially with running prover process.
7.9 */
7.10
7.11 package isabelle
7.12 @@ -16,6 +16,14 @@
7.13
7.14 object Session
7.15 {
7.16 + /* abstract file store */
7.17 +
7.18 + abstract class File_Store
7.19 + {
7.20 + def read(path: Path): String
7.21 + }
7.22 +
7.23 +
7.24 /* events */
7.25
7.26 case object Global_Settings
7.27 @@ -32,7 +40,7 @@
7.28 }
7.29
7.30
7.31 -class Session(val system: Isabelle_System)
7.32 +class Session(val system: Isabelle_System, val file_store: Session.File_Store)
7.33 {
7.34 /* real time parameters */ // FIXME properties or settings (!?)
7.35
7.36 @@ -116,6 +124,8 @@
7.37
7.38 /** main protocol actor **/
7.39
7.40 + /* global state */
7.41 +
7.42 @volatile private var syntax = new Outer_Syntax(system.symbols)
7.43 def current_syntax(): Outer_Syntax = syntax
7.44
7.45 @@ -134,15 +144,41 @@
7.46 private val global_state = new Volatile(Document.State.init)
7.47 def current_state(): Document.State = global_state.peek()
7.48
7.49 +
7.50 + /* theory files */
7.51 +
7.52 + val thy_header = new Thy_Header(system.symbols)
7.53 +
7.54 + val thy_load = new Thy_Load
7.55 + {
7.56 + override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
7.57 + {
7.58 + val file = system.platform_file(dir + Thy_Header.thy_path(name))
7.59 + if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
7.60 + val text = Standard_System.read_file(file)
7.61 + val header = thy_header.read(text)
7.62 + (text, header)
7.63 + }
7.64 + }
7.65 +
7.66 + val thy_info = new Thy_Info(thy_load)
7.67 +
7.68 +
7.69 + /* actor messages */
7.70 +
7.71 private case object Interrupt_Prover
7.72 - private case class Edit_Version(edits: List[Document.Edit_Text])
7.73 + private case class Edit_Node(thy_name: String,
7.74 + header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
7.75 + private case class Init_Node(thy_name: String,
7.76 + header: Exn.Result[Thy_Header.Header], text: String)
7.77 private case class Start(timeout: Time, args: List[String])
7.78
7.79 var verbose: Boolean = false
7.80
7.81 private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
7.82 {
7.83 - var prover: Isabelle_Process with Isar_Document = null
7.84 + val this_actor = self
7.85 + var prover: Option[Isabelle_Process with Isar_Document] = None
7.86
7.87
7.88 /* document changes */
7.89 @@ -174,7 +210,8 @@
7.90 case Some(command) =>
7.91 if (global_state.peek().lookup_command(command.id).isEmpty) {
7.92 global_state.change(_.define_command(command))
7.93 - prover.define_command(command.id, system.symbols.encode(command.source))
7.94 + prover.get.
7.95 + define_command(command.id, system.symbols.encode(command.source))
7.96 }
7.97 Some(command.id)
7.98 }
7.99 @@ -183,7 +220,7 @@
7.100 (name -> Some(ids))
7.101 }
7.102 global_state.change(_.define_version(version, former_assignment))
7.103 - prover.edit_version(previous.id, version.id, id_edits)
7.104 + prover.get.edit_version(previous.id, version.id, id_edits)
7.105 }
7.106 //}}}
7.107
7.108 @@ -241,47 +278,63 @@
7.109 //}}}
7.110
7.111
7.112 + def edit_version(edits: List[Document.Edit_Text])
7.113 + //{{{
7.114 + {
7.115 + val previous = global_state.peek().history.tip.version
7.116 + val syntax = current_syntax()
7.117 + val result = Future.fork { Thy_Syntax.text_edits(syntax, new_id _, previous.join, edits) }
7.118 + val change = global_state.change_yield(_.extend_history(previous, edits, result))
7.119 +
7.120 + change.version.map(_ => {
7.121 + assignments.await { global_state.peek().is_assigned(previous.get_finished) }
7.122 + this_actor ! change })
7.123 + }
7.124 + //}}}
7.125 +
7.126 +
7.127 /* main loop */
7.128
7.129 var finished = false
7.130 while (!finished) {
7.131 receive {
7.132 case Interrupt_Prover =>
7.133 - if (prover != null) prover.interrupt
7.134 + prover.map(_.interrupt)
7.135
7.136 - case Edit_Version(edits) if prover != null =>
7.137 - val previous = global_state.peek().history.tip.version
7.138 - val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
7.139 - val change = global_state.change_yield(_.extend_history(previous, edits, result))
7.140 -
7.141 - val this_actor = self
7.142 - change.version.map(_ => {
7.143 - assignments.await { global_state.peek().is_assigned(previous.get_finished) }
7.144 - this_actor ! change })
7.145 -
7.146 + case Edit_Node(thy_name, header, text_edits) if prover.isDefined =>
7.147 + edit_version(List((thy_name, Some(text_edits))))
7.148 reply(())
7.149
7.150 - case change: Document.Change if prover != null => handle_change(change)
7.151 + case Init_Node(thy_name, header, text) if prover.isDefined =>
7.152 + // FIXME compare with existing node
7.153 + edit_version(List(
7.154 + (thy_name, None),
7.155 + (thy_name, Some(List(Text.Edit.insert(0, text))))))
7.156 + reply(())
7.157 +
7.158 + case change: Document.Change if prover.isDefined =>
7.159 + handle_change(change)
7.160
7.161 case result: Isabelle_Process.Result => handle_result(result)
7.162
7.163 - case Start(timeout, args) if prover == null =>
7.164 + case Start(timeout, args) if prover.isEmpty =>
7.165 if (phase == Session.Inactive || phase == Session.Failed) {
7.166 phase = Session.Startup
7.167 - prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
7.168 + prover =
7.169 + Some(new Isabelle_Process(system, timeout, this_actor, args:_*) with Isar_Document)
7.170 }
7.171
7.172 case Stop =>
7.173 if (phase == Session.Ready) {
7.174 global_state.change(_ => Document.State.init) // FIXME event bus!?
7.175 phase = Session.Shutdown
7.176 - prover.terminate
7.177 + prover.get.terminate
7.178 phase = Session.Inactive
7.179 }
7.180 finished = true
7.181 reply(())
7.182
7.183 - case bad if prover != null =>
7.184 + case bad if prover.isDefined =>
7.185 System.err.println("session_actor: ignoring bad message " + bad)
7.186 }
7.187 }
7.188 @@ -297,7 +350,15 @@
7.189
7.190 def interrupt() { session_actor ! Interrupt_Prover }
7.191
7.192 - def edit_version(edits: List[Document.Edit_Text]) { session_actor !? Edit_Version(edits) }
7.193 + def edit_node(thy_name: String, header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
7.194 + {
7.195 + session_actor !? Edit_Node(thy_name, header, edits)
7.196 + }
7.197 +
7.198 + def init_node(thy_name: String, header: Exn.Result[Thy_Header.Header], text: String)
7.199 + {
7.200 + session_actor !? Init_Node(thy_name, header, text)
7.201 + }
7.202
7.203 def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
7.204 global_state.peek().snapshot(name, pending_edits)
8.1 --- a/src/Pure/Thy/thy_header.scala Mon Jul 04 10:23:46 2011 +0200
8.2 +++ b/src/Pure/Thy/thy_header.scala Mon Jul 04 16:54:58 2011 +0200
8.3 @@ -9,7 +9,7 @@
8.4
8.5 import scala.annotation.tailrec
8.6 import scala.collection.mutable
8.7 -import scala.util.parsing.input.Reader
8.8 +import scala.util.parsing.input.{Reader, CharSequenceReader}
8.9 import scala.util.matching.Regex
8.10
8.11 import java.io.File
8.12 @@ -36,8 +36,10 @@
8.13
8.14 /* file name */
8.15
8.16 - val Thy_Path1 = new Regex("([^/]*)\\.thy")
8.17 - val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
8.18 + def thy_path(name: String): Path = Path.basic(name).ext("thy")
8.19 +
8.20 + private val Thy_Path1 = new Regex("([^/]*)\\.thy")
8.21 + private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
8.22
8.23 def split_thy_path(path: String): Option[(String, String)] =
8.24 path match {
8.25 @@ -99,10 +101,24 @@
8.26 }
8.27 }
8.28
8.29 + def read(source: CharSequence): Header =
8.30 + read(new CharSequenceReader(source))
8.31 +
8.32 def read(file: File): Header =
8.33 {
8.34 val reader = Scan.byte_reader(file)
8.35 try { read(reader).decode_permissive_utf8 }
8.36 finally { reader.close }
8.37 }
8.38 +
8.39 +
8.40 + /* check */
8.41 +
8.42 + def check(name: String, source: CharSequence): Header =
8.43 + {
8.44 + val header = read(source)
8.45 + val name1 = header.name
8.46 + if (name == name1) header
8.47 + else error("Bad file name " + Thy_Header.thy_path(name) + " for theory " + quote(name1))
8.48 + }
8.49 }
9.1 --- a/src/Pure/Thy/thy_info.ML Mon Jul 04 10:23:46 2011 +0200
9.2 +++ b/src/Pure/Thy/thy_info.ML Mon Jul 04 16:54:58 2011 +0200
9.3 @@ -34,10 +34,11 @@
9.4 datatype action = Update | Remove;
9.5
9.6 local
9.7 - val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
9.8 + val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action -> string -> unit) list);
9.9 in
9.10 - fun add_hook f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change hooks (cons f));
9.11 - fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
9.12 + fun add_hook f = Synchronized.change hooks (cons f);
9.13 + fun perform action name =
9.14 + List.app (fn f => (try (fn () => f action name) (); ())) (Synchronized.value hooks);
9.15 end;
9.16
9.17
9.18 @@ -135,7 +136,7 @@
9.19
9.20 (** thy operations **)
9.21
9.22 -(* remove theory *)
9.23 +(* main loader actions *)
9.24
9.25 fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
9.26 if is_finished name then error (loader_msg "attempt to change finished theory" [name])
9.27 @@ -151,11 +152,23 @@
9.28 if known_thy name then remove_thy name
9.29 else ());
9.30
9.31 +fun update_thy deps theory = NAMED_CRITICAL "Thy_Info" (fn () =>
9.32 + let
9.33 + val name = Context.theory_name theory;
9.34 + val parents = map Context.theory_name (Theory.parents_of theory);
9.35 + val _ = kill_thy name;
9.36 + val _ = map get_theory parents;
9.37 + val _ = change_thys (new_entry name parents (SOME deps, SOME theory));
9.38 + val _ = perform Update name;
9.39 + in () end);
9.40 +
9.41
9.42 (* scheduling loader tasks *)
9.43
9.44 +type result = theory * unit future * (unit -> unit);
9.45 +
9.46 datatype task =
9.47 - Task of string list * (theory list -> (theory * unit future * (unit -> unit))) |
9.48 + Task of string list * (theory list -> result) |
9.49 Finished of theory;
9.50
9.51 fun task_finished (Task _) = false
9.52 @@ -163,15 +176,15 @@
9.53
9.54 local
9.55
9.56 +fun finish_thy ((thy, present, commit): result) =
9.57 + (Global_Theory.join_proofs thy; Future.join present; commit (); thy);
9.58 +
9.59 fun schedule_seq task_graph =
9.60 ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
9.61 (case Graph.get_node task_graph name of
9.62 Task (parents, body) =>
9.63 - let
9.64 - val (thy, present, commit) = body (map (the o Symtab.lookup tab) parents);
9.65 - val _ = Future.join present;
9.66 - val _ = commit ();
9.67 - in Symtab.update (name, thy) tab end
9.68 + let val result = body (map (the o Symtab.lookup tab) parents)
9.69 + in Symtab.update (name, finish_thy result) tab end
9.70 | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
9.71
9.72 fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
9.73 @@ -199,10 +212,8 @@
9.74 val _ =
9.75 tasks |> maps (fn name =>
9.76 let
9.77 - val (thy, present, commit) = Future.join (the (Symtab.lookup futures name));
9.78 - val _ = Global_Theory.join_proofs thy;
9.79 - val _ = Future.join present;
9.80 - val _ = commit ();
9.81 + val result = Future.join (the (Symtab.lookup futures name));
9.82 + val _ = finish_thy result;
9.83 in [] end handle exn => [Exn.Exn exn])
9.84 |> rev |> Exn.release_all;
9.85 in () end) ();
9.86 @@ -226,7 +237,7 @@
9.87 fun required_by _ [] = ""
9.88 | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
9.89
9.90 -fun load_thy initiators update_time (deps: deps) text name parent_thys =
9.91 +fun load_thy initiators update_time deps text name parent_thys =
9.92 let
9.93 val _ = kill_thy name;
9.94 val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
9.95 @@ -240,13 +251,7 @@
9.96 |> Present.begin_theory update_time dir uses;
9.97
9.98 val (theory, present) = Outer_Syntax.load_thy name init pos text;
9.99 -
9.100 - val parents = map Context.theory_name parent_thys;
9.101 - fun commit () =
9.102 - NAMED_CRITICAL "Thy_Info" (fn () =>
9.103 - (map get_theory parents;
9.104 - change_thys (new_entry name parents (SOME deps, SOME theory));
9.105 - perform Update name));
9.106 + fun commit () = update_thy deps theory;
9.107 in (theory, present, commit) end;
9.108
9.109 fun check_deps dir name =
9.110 @@ -274,13 +279,14 @@
9.111 let
9.112 val path = Path.expand (Path.explode str);
9.113 val name = Path.implode (Path.base path);
9.114 - val dir' = Path.append dir (Path.dir path);
9.115 - val _ = member (op =) initiators name andalso error (cycle_msg initiators);
9.116 in
9.117 (case try (Graph.get_node tasks) name of
9.118 SOME task => (task_finished task, tasks)
9.119 | NONE =>
9.120 let
9.121 + val dir' = Path.append dir (Path.dir path);
9.122 + val _ = member (op =) initiators name andalso error (cycle_msg initiators);
9.123 +
9.124 val (current, deps, imports) = check_deps dir' name
9.125 handle ERROR msg => cat_error msg
9.126 (loader_msg "the error(s) above occurred while examining theory" [name] ^
9.127 @@ -332,16 +338,12 @@
9.128 let
9.129 val name = Context.theory_name theory;
9.130 val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
9.131 - val parents = map Context.theory_name (Theory.parents_of theory);
9.132 val imports = Thy_Load.imports_of theory;
9.133 - val deps = make_deps master imports;
9.134 in
9.135 NAMED_CRITICAL "Thy_Info" (fn () =>
9.136 (kill_thy name;
9.137 Output.urgent_message ("Registering theory " ^ quote name);
9.138 - map get_theory parents;
9.139 - change_thys (new_entry name parents (SOME deps, SOME theory));
9.140 - perform Update name))
9.141 + update_thy (make_deps master imports) theory))
9.142 end;
9.143
9.144
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/Pure/Thy/thy_info.scala Mon Jul 04 16:54:58 2011 +0200
10.3 @@ -0,0 +1,59 @@
10.4 +/* Title: Pure/Thy/thy_info.scala
10.5 + Author: Makarius
10.6 +
10.7 +Theory and file dependencies.
10.8 +*/
10.9 +
10.10 +package isabelle
10.11 +
10.12 +
10.13 +class Thy_Info(thy_load: Thy_Load)
10.14 +{
10.15 + /* messages */
10.16 +
10.17 + private def show_path(names: List[String]): String =
10.18 + names.map(quote).mkString(" via ")
10.19 +
10.20 + private def cycle_msg(names: List[String]): String =
10.21 + "Cyclic dependency of " + show_path(names)
10.22 +
10.23 + private def required_by(s: String, initiators: List[String]): String =
10.24 + if (initiators.isEmpty) ""
10.25 + else s + "(required by " + show_path(initiators.reverse) + ")"
10.26 +
10.27 +
10.28 + /* dependencies */
10.29 +
10.30 + type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header)
10.31 +
10.32 + private def require_thys(
10.33 + initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
10.34 + (deps /: strs)(require_thy(initiators, dir, _, _))
10.35 +
10.36 + private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
10.37 + {
10.38 + val path = Path.explode(str)
10.39 + val name = path.base.implode
10.40 +
10.41 + if (deps.isDefinedAt(name)) deps
10.42 + else {
10.43 + val dir1 = dir + path.dir
10.44 + try {
10.45 + if (initiators.contains(name)) error(cycle_msg(initiators))
10.46 + val (text, header) =
10.47 + try { thy_load.check_thy(dir1, name) }
10.48 + catch {
10.49 + case ERROR(msg) =>
10.50 + cat_error(msg, "The error(s) above occurred while examining theory " +
10.51 + quote(name) + required_by("\n", initiators))
10.52 + }
10.53 + require_thys(name :: initiators, dir1,
10.54 + deps + (name -> Exn.Res(text, header)), header.imports)
10.55 + }
10.56 + catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
10.57 + }
10.58 + }
10.59 +
10.60 + def dependencies(dir: Path, str: String): Deps =
10.61 + require_thy(Nil, dir, Map.empty, str) // FIXME capture errors in str (!??)
10.62 +}
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Pure/Thy/thy_load.scala Mon Jul 04 16:54:58 2011 +0200
11.3 @@ -0,0 +1,13 @@
11.4 +/* Title: Pure/Thy/thy_load.scala
11.5 + Author: Makarius
11.6 +
11.7 +Loading files that contribute to a theory.
11.8 +*/
11.9 +
11.10 +package isabelle
11.11 +
11.12 +abstract class Thy_Load
11.13 +{
11.14 + def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
11.15 +}
11.16 +
12.1 --- a/src/Pure/Thy/thy_syntax.scala Mon Jul 04 10:23:46 2011 +0200
12.2 +++ b/src/Pure/Thy/thy_syntax.scala Mon Jul 04 16:54:58 2011 +0200
12.3 @@ -99,7 +99,7 @@
12.4
12.5 /** text edits **/
12.6
12.7 - def text_edits(session: Session, previous: Document.Version,
12.8 + def text_edits(syntax: Outer_Syntax, new_id: () => Document.ID, previous: Document.Version,
12.9 edits: List[Document.Edit_Text]): (List[Document.Edit_Command], Document.Version) =
12.10 {
12.11 /* phase 1: edit individual command source */
12.12 @@ -147,7 +147,7 @@
12.13 commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
12.14
12.15 val sources = range.flatMap(_.span.map(_.source))
12.16 - val spans0 = parse_spans(session.current_syntax().scan(sources.mkString))
12.17 + val spans0 = parse_spans(syntax.scan(sources.mkString))
12.18
12.19 val (before_edit, spans1) =
12.20 if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
12.21 @@ -159,7 +159,7 @@
12.22 (Some(last), spans1.take(spans1.length - 1))
12.23 else (commands.next(last), spans1)
12.24
12.25 - val inserted = spans2.map(span => new Command(session.new_id(), span))
12.26 + val inserted = spans2.map(span => new Command(new_id(), span))
12.27 val new_commands =
12.28 commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
12.29 recover_spans(new_commands)
12.30 @@ -195,7 +195,7 @@
12.31 doc_edits += (name -> Some(cmd_edits))
12.32 nodes += (name -> new Document.Node(commands2))
12.33 }
12.34 - (doc_edits.toList, new Document.Version(session.new_id(), nodes))
12.35 + (doc_edits.toList, new Document.Version(new_id(), nodes))
12.36 }
12.37 }
12.38 }
13.1 --- a/src/Pure/build-jars Mon Jul 04 10:23:46 2011 +0200
13.2 +++ b/src/Pure/build-jars Mon Jul 04 16:54:58 2011 +0200
13.3 @@ -50,6 +50,8 @@
13.4 Thy/completion.scala
13.5 Thy/html.scala
13.6 Thy/thy_header.scala
13.7 + Thy/thy_info.scala
13.8 + Thy/thy_load.scala
13.9 Thy/thy_syntax.scala
13.10 library.scala
13.11 package.scala
14.1 --- a/src/Pure/library.ML Mon Jul 04 10:23:46 2011 +0200
14.2 +++ b/src/Pure/library.ML Mon Jul 04 16:54:58 2011 +0200
14.3 @@ -28,7 +28,7 @@
14.4 val funpow: int -> ('a -> 'a) -> 'a -> 'a
14.5 val funpow_yield: int -> ('a -> 'b * 'a) -> 'a -> 'b list * 'a
14.6
14.7 - (*errors*)
14.8 + (*user errors*)
14.9 exception ERROR of string
14.10 val error: string -> 'a
14.11 val cat_error: string -> string -> 'a
14.12 @@ -260,7 +260,7 @@
14.13 | funpow_yield n f x = x |> f ||>> funpow_yield (n - 1) f |>> op ::;
14.14
14.15
14.16 -(* errors *)
14.17 +(* user errors *)
14.18
14.19 exception ERROR of string;
14.20 fun error msg = raise ERROR msg;
15.1 --- a/src/Pure/library.scala Mon Jul 04 10:23:46 2011 +0200
15.2 +++ b/src/Pure/library.scala Mon Jul 04 16:54:58 2011 +0200
15.3 @@ -18,6 +18,27 @@
15.4
15.5 object Library
15.6 {
15.7 + /* user errors */
15.8 +
15.9 + object ERROR
15.10 + {
15.11 + def apply(message: String): Throwable = new RuntimeException(message)
15.12 + def unapply(exn: Throwable): Option[String] =
15.13 + exn match {
15.14 + case e: RuntimeException =>
15.15 + val msg = e.getMessage
15.16 + Some(if (msg == null) "" else msg)
15.17 + case _ => None
15.18 + }
15.19 + }
15.20 +
15.21 + def error(message: String): Nothing = throw ERROR(message)
15.22 +
15.23 + def cat_error(msg1: String, msg2: String): Nothing =
15.24 + if (msg1 == "") error(msg1)
15.25 + else error(msg1 + "\n" + msg2)
15.26 +
15.27 +
15.28 /* lists */
15.29
15.30 def separate[A](s: A, list: List[A]): List[A] =
15.31 @@ -41,39 +62,7 @@
15.32 }
15.33
15.34
15.35 - /* strings */
15.36 -
15.37 - def quote(s: String): String = "\"" + s + "\""
15.38 - def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
15.39 - def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
15.40 -
15.41 -
15.42 - /* reverse CharSequence */
15.43 -
15.44 - class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
15.45 - {
15.46 - require(0 <= start && start <= end && end <= text.length)
15.47 -
15.48 - def this(text: CharSequence) = this(text, 0, text.length)
15.49 -
15.50 - def length: Int = end - start
15.51 - def charAt(i: Int): Char = text.charAt(end - i - 1)
15.52 -
15.53 - def subSequence(i: Int, j: Int): CharSequence =
15.54 - if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
15.55 - else throw new IndexOutOfBoundsException
15.56 -
15.57 - override def toString: String =
15.58 - {
15.59 - val buf = new StringBuilder(length)
15.60 - for (i <- 0 until length)
15.61 - buf.append(charAt(i))
15.62 - buf.toString
15.63 - }
15.64 - }
15.65 -
15.66 -
15.67 - /* iterate over chunks (cf. space_explode/split_lines in ML) */
15.68 + /* iterate over chunks (cf. space_explode) */
15.69
15.70 def chunks(source: CharSequence, sep: Char = '\n') = new Iterator[CharSequence]
15.71 {
15.72 @@ -104,6 +93,38 @@
15.73 }
15.74
15.75
15.76 + /* strings */
15.77 +
15.78 + def quote(s: String): String = "\"" + s + "\""
15.79 + def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
15.80 + def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
15.81 +
15.82 +
15.83 + /* reverse CharSequence */
15.84 +
15.85 + class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
15.86 + {
15.87 + require(0 <= start && start <= end && end <= text.length)
15.88 +
15.89 + def this(text: CharSequence) = this(text, 0, text.length)
15.90 +
15.91 + def length: Int = end - start
15.92 + def charAt(i: Int): Char = text.charAt(end - i - 1)
15.93 +
15.94 + def subSequence(i: Int, j: Int): CharSequence =
15.95 + if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
15.96 + else throw new IndexOutOfBoundsException
15.97 +
15.98 + override def toString: String =
15.99 + {
15.100 + val buf = new StringBuilder(length)
15.101 + for (i <- 0 until length)
15.102 + buf.append(charAt(i))
15.103 + buf.toString
15.104 + }
15.105 + }
15.106 +
15.107 +
15.108 /* simple dialogs */
15.109
15.110 private def simple_dialog(kind: Int, default_title: String)
15.111 @@ -160,3 +181,17 @@
15.112 Exn.release(result)
15.113 }
15.114 }
15.115 +
15.116 +
15.117 +class Basic_Library
15.118 +{
15.119 + val space_explode = Library.space_explode _
15.120 +
15.121 + val quote = Library.quote _
15.122 + val commas = Library.commas _
15.123 + val commas_quote = Library.commas_quote _
15.124 +
15.125 + val ERROR = Library.ERROR
15.126 + val error = Library.error _
15.127 + val cat_error = Library.cat_error _
15.128 +}
16.1 --- a/src/Pure/package.scala Mon Jul 04 10:23:46 2011 +0200
16.2 +++ b/src/Pure/package.scala Mon Jul 04 16:54:58 2011 +0200
16.3 @@ -4,8 +4,7 @@
16.4 Toplevel isabelle package.
16.5 */
16.6
16.7 -package object isabelle
16.8 +package object isabelle extends isabelle.Basic_Library
16.9 {
16.10 - def error(message: String): Nothing = throw new RuntimeException(message)
16.11 }
16.12
17.1 --- a/src/Tools/jEdit/src/document_model.scala Mon Jul 04 10:23:46 2011 +0200
17.2 +++ b/src/Tools/jEdit/src/document_model.scala Mon Jul 04 16:54:58 2011 +0200
17.3 @@ -45,10 +45,10 @@
17.4 }
17.5 }
17.6
17.7 - def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
17.8 + def init(session: Session, buffer: Buffer, master_dir: String, thy_name: String): Document_Model =
17.9 {
17.10 exit(buffer)
17.11 - val model = new Document_Model(session, buffer, thy_name)
17.12 + val model = new Document_Model(session, buffer, master_dir, thy_name)
17.13 buffer.setProperty(key, model)
17.14 model.activate()
17.15 model
17.16 @@ -56,31 +56,36 @@
17.17 }
17.18
17.19
17.20 -class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
17.21 +class Document_Model(val session: Session,
17.22 + val buffer: Buffer, val master_dir: String, val thy_name: String)
17.23 {
17.24 /* pending text edits */
17.25
17.26 - object pending_edits // owned by Swing thread
17.27 + private def capture_header(): Exn.Result[Thy_Header.Header] =
17.28 + Exn.capture {
17.29 + session.thy_header.check(thy_name, buffer.getSegment(0, buffer.getLength))
17.30 + }
17.31 +
17.32 + private object pending_edits // owned by Swing thread
17.33 {
17.34 private val pending = new mutable.ListBuffer[Text.Edit]
17.35 def snapshot(): List[Text.Edit] = pending.toList
17.36
17.37 - def flush(more_edits: Option[List[Text.Edit]]*)
17.38 + def flush()
17.39 {
17.40 Swing_Thread.require()
17.41 - val edits = snapshot()
17.42 - pending.clear
17.43 -
17.44 - val all_edits =
17.45 - if (edits.isEmpty) more_edits.toList
17.46 - else Some(edits) :: more_edits.toList
17.47 - if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
17.48 + snapshot() match {
17.49 + case Nil =>
17.50 + case edits =>
17.51 + pending.clear
17.52 + session.edit_node(master_dir + "/" + thy_name, capture_header(), edits)
17.53 + }
17.54 }
17.55
17.56 def init()
17.57 {
17.58 - Swing_Thread.require()
17.59 - flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
17.60 + flush()
17.61 + session.init_node(master_dir + "/" + thy_name, capture_header(), Isabelle.buffer_text(buffer))
17.62 }
17.63
17.64 private val delay_flush =
17.65 @@ -100,7 +105,7 @@
17.66 def snapshot(): Document.Snapshot =
17.67 {
17.68 Swing_Thread.require()
17.69 - session.snapshot(thy_name, pending_edits.snapshot())
17.70 + session.snapshot(master_dir + "/" + thy_name, pending_edits.snapshot())
17.71 }
17.72
17.73
18.1 --- a/src/Tools/jEdit/src/document_view.scala Mon Jul 04 10:23:46 2011 +0200
18.2 +++ b/src/Tools/jEdit/src/document_view.scala Mon Jul 04 16:54:58 2011 +0200
18.3 @@ -78,7 +78,7 @@
18.4 Swing_Thread.require()
18.5 if (model.buffer == text_area.getBuffer) body
18.6 else {
18.7 - Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
18.8 + Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
18.9 default
18.10 }
18.11 }
19.1 --- a/src/Tools/jEdit/src/plugin.scala Mon Jul 04 10:23:46 2011 +0200
19.2 +++ b/src/Tools/jEdit/src/plugin.scala Mon Jul 04 16:54:58 2011 +0200
19.3 @@ -10,14 +10,14 @@
19.4 import isabelle._
19.5
19.6 import java.lang.System
19.7 -import java.io.{FileInputStream, IOException}
19.8 +import java.io.{File, FileInputStream, IOException}
19.9 import java.awt.Font
19.10
19.11 import scala.collection.mutable
19.12 import scala.swing.ComboBox
19.13
19.14 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
19.15 - Buffer, EditPane, ServiceManager, View}
19.16 + Buffer, EditPane, MiscUtilities, ServiceManager, View}
19.17 import org.gjt.sp.jedit.buffer.JEditBuffer
19.18 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
19.19 import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
19.20 @@ -201,8 +201,8 @@
19.21 case None =>
19.22 // FIXME strip protocol prefix of URL
19.23 Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
19.24 - case Some((dir, thy_name)) =>
19.25 - Some(Document_Model.init(session, buffer, dir + "/" + thy_name))
19.26 + case Some((master_dir, thy_name)) =>
19.27 + Some(Document_Model.init(session, buffer, master_dir, thy_name))
19.28 case None => None
19.29 }
19.30 }
19.31 @@ -314,15 +314,30 @@
19.32
19.33 class Plugin extends EBPlugin
19.34 {
19.35 - /* session management */
19.36 + /* editor file store */
19.37
19.38 - @volatile private var session_ready = false
19.39 + private val file_store = new Session.File_Store
19.40 + {
19.41 + def read(path: Path): String =
19.42 + {
19.43 + val platform_path = Isabelle.system.platform_path(path)
19.44 + val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
19.45 +
19.46 + Isabelle.jedit_buffers().find(buffer =>
19.47 + MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match {
19.48 + case Some(buffer) => Isabelle.buffer_text(buffer)
19.49 + case None => Standard_System.read_file(new File(platform_path))
19.50 + }
19.51 + }
19.52 + }
19.53 +
19.54 +
19.55 + /* session manager */
19.56
19.57 private val session_manager = actor {
19.58 loop {
19.59 react {
19.60 case phase: Session.Phase =>
19.61 - session_ready = phase == Session.Ready
19.62 phase match {
19.63 case Session.Failed =>
19.64 Swing_Thread.now {
19.65 @@ -335,7 +350,6 @@
19.66 case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
19.67 case _ =>
19.68 }
19.69 -
19.70 case bad => System.err.println("session_manager: ignoring bad message " + bad)
19.71 }
19.72 }
19.73 @@ -357,7 +371,7 @@
19.74 if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
19.75
19.76 val buffer = msg.getBuffer
19.77 - if (buffer != null && session_ready)
19.78 + if (buffer != null && Isabelle.session.is_ready)
19.79 Isabelle.init_model(buffer)
19.80
19.81 case msg: EditPaneUpdate
19.82 @@ -373,7 +387,7 @@
19.83 if (buffer != null && text_area != null) {
19.84 if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
19.85 msg.getWhat == EditPaneUpdate.CREATED) {
19.86 - if (session_ready)
19.87 + if (Isabelle.session.is_ready)
19.88 Isabelle.init_view(buffer, text_area)
19.89 }
19.90 else Isabelle.exit_view(buffer, text_area)
19.91 @@ -393,7 +407,7 @@
19.92 Isabelle.setup_tooltips()
19.93 Isabelle.system = new Isabelle_System
19.94 Isabelle.system.install_fonts()
19.95 - Isabelle.session = new Session(Isabelle.system)
19.96 + Isabelle.session = new Session(Isabelle.system, file_store)
19.97 SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender(Isabelle.system.symbols))
19.98 if (ModeProvider.instance.isInstanceOf[ModeProvider])
19.99 ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)