1.1 --- a/src/Pure/General/markup.ML	Tue Jul 05 22:38:44 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Tue Jul 05 22:39:15 2011 +0200
     1.3 @@ -92,6 +92,7 @@
     1.4    val command_spanN: string val command_span: string -> T
     1.5    val ignored_spanN: string val ignored_span: T
     1.6    val malformed_spanN: string val malformed_span: T
     1.7 +  val loaded_theoryN: string val loaded_theory: string -> T
     1.8    val elapsedN: string
     1.9    val cpuN: string
    1.10    val gcN: string
    1.11 @@ -305,6 +306,11 @@
    1.12  val (malformed_spanN, malformed_span) = markup_elem "malformed_span";
    1.13  
    1.14  
    1.15 +(* theory loader *)
    1.16 +
    1.17 +val (loaded_theoryN, loaded_theory) = markup_string "loaded_theory" nameN;
    1.18 +
    1.19 +
    1.20  (* timing *)
    1.21  
    1.22  val timingN = "timing";

     2.1 --- a/src/Pure/General/markup.scala	Tue Jul 05 22:38:44 2011 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Tue Jul 05 22:39:15 2011 +0200
     2.3 @@ -246,6 +246,11 @@
     2.4    val MALFORMED_SPAN = "malformed_span"
     2.5  
     2.6  
     2.7 +  /* theory loader */
     2.8 +
     2.9 +  val LOADED_THEORY = "loaded_theory"
    2.10 +
    2.11 +
    2.12    /* timing */
    2.13  
    2.14    val TIMING = "timing"

     3.1 --- a/src/Pure/System/isabelle_process.ML	Tue Jul 05 22:38:44 2011 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jul 05 22:39:15 2011 +0200
     3.3 @@ -180,6 +180,7 @@
     3.4  
     3.5      val in_stream = setup_channels in_fifo out_fifo;
     3.6      val _ = Keyword.status ();
     3.7 +    val _ = Thy_Info.status ();
     3.8      val _ = Output.status (Markup.markup Markup.ready "process ready");
     3.9    in loop in_stream end));
    3.10  

     4.1 --- a/src/Pure/System/session.scala	Tue Jul 05 22:38:44 2011 +0200
     4.2 +++ b/src/Pure/System/session.scala	Tue Jul 05 22:39:15 2011 +0200
     4.3 @@ -115,6 +115,8 @@
     4.4  
     4.5    /* global state */
     4.6  
     4.7 +  @volatile var loaded_theories: Set[String] = Set()
     4.8 +
     4.9    @volatile private var syntax = new Outer_Syntax(Isabelle_System.symbols)
    4.10    def current_syntax(): Outer_Syntax = syntax
    4.11  
    4.12 @@ -138,6 +140,9 @@
    4.13  
    4.14    val thy_load = new Thy_Load
    4.15    {
    4.16 +    override def is_loaded(name: String): Boolean =
    4.17 +      loaded_theories.contains(name)
    4.18 +
    4.19      override def check_thy(dir: Path, name: String): (String, Thy_Header.Header) =
    4.20      {
    4.21        val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
    4.22 @@ -255,6 +260,7 @@
    4.23                  catch { case _: Document.State.Fail => bad_result(result) }
    4.24                case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
    4.25                case List(Keyword.Keyword_Decl(name)) => syntax += name
    4.26 +              case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
    4.27                case _ => bad_result(result)
    4.28              }
    4.29            }

     5.1 --- a/src/Pure/Thy/thy_info.ML	Tue Jul 05 22:38:44 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Jul 05 22:39:15 2011 +0200
     5.3 @@ -10,6 +10,7 @@
     5.4    datatype action = Update | Remove
     5.5    val add_hook: (action -> string -> unit) -> unit
     5.6    val get_names: unit -> string list
     5.7 +  val status: unit -> unit
     5.8    val lookup_theory: string -> theory option
     5.9    val get_theory: string -> theory
    5.10    val is_finished: string -> bool
    5.11 @@ -88,6 +89,9 @@
    5.12  
    5.13  fun get_names () = Graph.topological_order (get_thys ());
    5.14  
    5.15 +fun status () =
    5.16 +  List.app (Output.status o Markup.markup_only o Markup.loaded_theory) (get_names ());
    5.17 +
    5.18  
    5.19  (* access thy *)
    5.20  

     6.1 --- a/src/Pure/Thy/thy_info.scala	Tue Jul 05 22:38:44 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Jul 05 22:39:15 2011 +0200
     6.3 @@ -7,6 +7,20 @@
     6.4  package isabelle
     6.5  
     6.6  
     6.7 +object Thy_Info
     6.8 +{
     6.9 +  /* protocol messages */
    6.10 +
    6.11 +  object Loaded_Theory {
    6.12 +    def unapply(msg: XML.Tree): Option[String] =
    6.13 +      msg match {
    6.14 +        case XML.Elem(Markup(Markup.LOADED_THEORY, List((Markup.NAME, name))), _) => Some(name)
    6.15 +        case _ => None
    6.16 +      }
    6.17 +  }
    6.18 +}
    6.19 +
    6.20 +
    6.21  class Thy_Info(thy_load: Thy_Load)
    6.22  {
    6.23    /* messages */
    6.24 @@ -26,16 +40,17 @@
    6.25  
    6.26    type Deps = Map[String, Exn.Result[(String, Thy_Header.Header)]]  // name -> (text, header)
    6.27  
    6.28 -  private def require_thys(
    6.29 +  private def require_thys(ignored: String => Boolean,
    6.30        initiators: List[String], dir: Path, deps: Deps, strs: List[String]): Deps =
    6.31 -    (deps /: strs)(require_thy(initiators, dir, _, _))
    6.32 +    (deps /: strs)(require_thy(ignored, initiators, dir, _, _))
    6.33  
    6.34 -  private def require_thy(initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
    6.35 +  private def require_thy(ignored: String => Boolean,
    6.36 +      initiators: List[String], dir: Path, deps: Deps, str: String): Deps =
    6.37    {
    6.38      val path = Path.explode(str)
    6.39      val name = path.base.implode
    6.40  
    6.41 -    if (deps.isDefinedAt(name)) deps
    6.42 +    if (deps.isDefinedAt(name) || ignored(name)) deps
    6.43      else {
    6.44        val dir1 = dir + path.dir
    6.45        try {
    6.46 @@ -47,7 +62,7 @@
    6.47                cat_error(msg, "The error(s) above occurred while examining theory " +
    6.48                  quote(name) + required_by("\n", initiators))
    6.49            }
    6.50 -        require_thys(name :: initiators, dir1,
    6.51 +        require_thys(ignored, name :: initiators, dir1,
    6.52            deps + (name -> Exn.Res(text, header)), header.imports)
    6.53        }
    6.54        catch { case e: Throwable => deps + (name -> Exn.Exn(e)) }
    6.55 @@ -55,5 +70,5 @@
    6.56    }
    6.57  
    6.58    def dependencies(dir: Path, str: String): Deps =
    6.59 -    require_thy(Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
    6.60 +    require_thy(thy_load.is_loaded, Nil, dir, Map.empty, str)  // FIXME capture errors in str (!??)
    6.61  }

     7.1 --- a/src/Pure/Thy/thy_load.scala	Tue Jul 05 22:38:44 2011 +0200
     7.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Jul 05 22:39:15 2011 +0200
     7.3 @@ -8,6 +8,8 @@
     7.4  
     7.5  abstract class Thy_Load
     7.6  {
     7.7 +  def is_loaded(name: String): Boolean
     7.8 +
     7.9    def check_thy(dir: Path, name: String): (String, Thy_Header.Header)
    7.10  }
    7.11