some support for theory files within Isabelle/Scala session;
authorwenzelm
Mon Jul 04 16:27:11 2011 +0200 (2011-07-04 ago)
changeset 43651511df47bcadc
parent 43650 f00da558b78e
child 43652 dcd0b667f73d
some support for theory files within Isabelle/Scala session;
src/Pure/System/session.scala
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.scala
src/Pure/build-jars
src/Pure/package.scala
     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