1.1 --- a/src/Pure/System/session.scala Mon Jul 04 13:43:10 2011 +0200
1.2 +++ b/src/Pure/System/session.scala Mon Jul 04 16:27:11 2011 +0200
1.3 @@ -2,7 +2,7 @@
1.4 Author: Makarius
1.5 Options: :folding=explicit:collapseFolds=1:
1.6
1.7 -Isabelle session, potentially with running prover.
1.8 +Main Isabelle/Scala session, potentially with running prover process.
1.9 */
1.10
1.11 package isabelle
1.12 @@ -124,7 +124,7 @@
1.13
1.14 /** main protocol actor **/
1.15
1.16 - val thy_header = new Thy_Header(system.symbols)
1.17 + /* global state */
1.18
1.19 @volatile private var syntax = new Outer_Syntax(system.symbols)
1.20 def current_syntax(): Outer_Syntax = syntax
1.21 @@ -144,6 +144,28 @@
1.22 private val global_state = new Volatile(Document.State.init)
1.23 def current_state(): Document.State = global_state.peek()
1.24
1.25 +
1.26 + /* theory files */
1.27 +
1.28 + val thy_header = new Thy_Header(system.symbols)
1.29 +
1.30 + val thy_load = new Thy_Load
1.31 + {
1.32 + override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
1.33 + {
1.34 + val file = system.platform_file(dir + Thy_Header.thy_path(name))
1.35 + if (!file.exists || !file.isFile) error("No such file: " + Library.quote(file.toString))
1.36 + val text = Standard_System.read_file(file)
1.37 + val header = thy_header.read(text)
1.38 + (text, header)
1.39 + }
1.40 + }
1.41 +
1.42 + val thy_info = new Thy_Info(thy_load)
1.43 +
1.44 +
1.45 + /* actor messages */
1.46 +
1.47 private case object Interrupt_Prover
1.48 private case class Edit_Node(thy_name: String,
1.49 header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
2.1 --- a/src/Pure/Thy/thy_info.ML Mon Jul 04 13:43:10 2011 +0200
2.2 +++ b/src/Pure/Thy/thy_info.ML Mon Jul 04 16:27:11 2011 +0200
2.3 @@ -279,13 +279,14 @@
2.4 let
2.5 val path = Path.expand (Path.explode str);
2.6 val name = Path.implode (Path.base path);
2.7 - val dir' = Path.append dir (Path.dir path);
2.8 - val _ = member (op =) initiators name andalso error (cycle_msg initiators);
2.9 in
2.10 (case try (Graph.get_node tasks) name of
2.11 SOME task => (task_finished task, tasks)
2.12 | NONE =>
2.13 let
2.14 + val dir' = Path.append dir (Path.dir path);
2.15 + val _ = member (op =) initiators name andalso error (cycle_msg initiators);
2.16 +
2.17 val (current, deps, imports) = check_deps dir' name
2.18 handle ERROR msg => cat_error msg
2.19 (loader_msg "the error(s) above occurred while examining theory" [name] ^
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/Pure/Thy/thy_info.scala Mon Jul 04 16:27:11 2011 +0200
3.3 @@ -0,0 +1,59 @@
3.4 +/* Title: Pure/Thy/thy_info.scala
3.5 + Author: Makarius
3.6 +
3.7 +Theory and file dependencies.
3.8 +*/
3.9 +
3.10 +package isabelle
3.11 +
3.12 +
3.13 +class Thy_Info(thy_load: Thy_Load)
3.14 +{
3.15 + /* messages */
3.16 +
3.17 + private def show_path(names: List[String]): String =
3.18 + names.map(Library.quote).mkString(" via ")
3.19 +
3.20 + private def cycle_msg(names: List[String]): String =
3.21 + "Cyclic dependency of " + show_path(names)
3.22 +
3.23 + private def required_by(s: String, initiators: List[String]): String =
3.24 + if (initiators.isEmpty) ""
3.25 + else s + "(required by " + show_path(initiators.reverse) + ")"
3.26 +
3.27 +
3.28 + /* dependencies */
3.29 +
3.30 + type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]] // name -> (text, header)
3.31 +
3.32 + private def require_thys(
3.33 + initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
3.34 + (deps /: strs)(require_thy(initiators, dir, _, _))
3.35 +
3.36 + private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
3.37 + {
3.38 + val path = Path.explode(str)
3.39 + val name = path.base.implode
3.40 +
3.41 + if (deps.isDefinedAt(name)) deps
3.42 + else {
3.43 + val dir1 = dir + path.dir
3.44 + try {
3.45 + if (initiators.contains(name)) error(cycle_msg(initiators))
3.46 + val (text, header) =
3.47 + try { thy_load.check_thy(dir1, name) }
3.48 + catch {
3.49 + case ERROR(msg) =>
3.50 + cat_error(msg, "The error(s) above occurred while examining theory " +
3.51 + Library.quote(name) + required_by("\n", initiators))
3.52 + }
3.53 + require_thys(name :: initiators, dir1,
3.54 + deps + (name -> Exn.Res(text, header)), header.imports)
3.55 + }
3.56 + catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
3.57 + }
3.58 + }
3.59 +
3.60 + def dependencies(dir: Path, str: String): Deps =
3.61 + require_thy(Nil, dir, Map.empty, str) // FIXME capture errors in str (!??)
3.62 +}
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/Thy/thy_load.scala Mon Jul 04 16:27:11 2011 +0200
4.3 @@ -0,0 +1,13 @@
4.4 +/* Title: Pure/Thy/thy_load.scala
4.5 + Author: Makarius
4.6 +
4.7 +Loading files that contribute to a theory.
4.8 +*/
4.9 +
4.10 +package isabelle
4.11 +
4.12 +abstract class Thy_Load
4.13 +{
4.14 + def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
4.15 +}
4.16 +
5.1 --- a/src/Pure/build-jars Mon Jul 04 13:43:10 2011 +0200
5.2 +++ b/src/Pure/build-jars Mon Jul 04 16:27:11 2011 +0200
5.3 @@ -50,6 +50,8 @@
5.4 Thy/completion.scala
5.5 Thy/html.scala
5.6 Thy/thy_header.scala
5.7 + Thy/thy_info.scala
5.8 + Thy/thy_load.scala
5.9 Thy/thy_syntax.scala
5.10 library.scala
5.11 package.scala
6.1 --- a/src/Pure/package.scala Mon Jul 04 13:43:10 2011 +0200
6.2 +++ b/src/Pure/package.scala Mon Jul 04 16:27:11 2011 +0200
6.3 @@ -6,6 +6,8 @@
6.4
6.5 package object isabelle
6.6 {
6.7 + /* errors */
6.8 +
6.9 object ERROR
6.10 {
6.11 def apply(message: String): Throwable = new RuntimeException(message)
6.12 @@ -17,6 +19,11 @@
6.13 case _ => None
6.14 }
6.15 }
6.16 +
6.17 def error(message: String): Nothing = throw ERROR(message)
6.18 +
6.19 + def cat_error(msg1: String, msg2: String): Nothing =
6.20 + if (msg1 == "") error(msg1)
6.21 + else error(msg1 + "\n" + msg2)
6.22 }
6.23