prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
authorwenzelm
Tue Aug 07 17:08:22 2012 +0200 (2012-08-07 ago)
changeset 487105b51ccdc8623
parent 48709 719f458cd89e
child 48711 8d381fdef898
prefer static Build.session_content for loaded theories -- discontinued incremental protocol;
src/Pure/PIDE/isabelle_markup.ML
src/Pure/PIDE/isabelle_markup.scala
src/Pure/System/build.scala
src/Pure/System/isabelle_process.ML
src/Pure/System/session.scala
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.scala
     1.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 16:34:15 2012 +0200
     1.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Tue Aug 07 17:08:22 2012 +0200
     1.3 @@ -103,7 +103,6 @@
     1.4    val badN: string val bad: Markup.T
     1.5    val functionN: string
     1.6    val ready: Properties.T
     1.7 -  val loaded_theory: string -> Properties.T
     1.8    val assign_execs: Properties.T
     1.9    val removed_versions: Properties.T
    1.10    val invoke_scala: string -> string -> Properties.T
    1.11 @@ -308,8 +307,6 @@
    1.12  
    1.13  val ready = [(functionN, "ready")];
    1.14  
    1.15 -fun loaded_theory name = [(functionN, "loaded_theory"), (Markup.nameN, name)];
    1.16 -
    1.17  val assign_execs = [(functionN, "assign_execs")];
    1.18  val removed_versions = [(functionN, "removed_versions")];
    1.19  
     2.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 16:34:15 2012 +0200
     2.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Tue Aug 07 17:08:22 2012 +0200
     2.3 @@ -252,15 +252,6 @@
     2.4  
     2.5    val Ready: Properties.T = List((FUNCTION, "ready"))
     2.6  
     2.7 -  object Loaded_Theory
     2.8 -  {
     2.9 -    def unapply(props: Properties.T): Option[String] =
    2.10 -      props match {
    2.11 -        case List((FUNCTION, "loaded_theory"), (Markup.NAME, name)) => Some(name)
    2.12 -        case _ => None
    2.13 -      }
    2.14 -  }
    2.15 -
    2.16    val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
    2.17    val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
    2.18  
     3.1 --- a/src/Pure/System/build.scala	Tue Aug 07 16:34:15 2012 +0200
     3.2 +++ b/src/Pure/System/build.scala	Tue Aug 07 17:08:22 2012 +0200
     3.3 @@ -315,22 +315,22 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* source dependencies */
     3.8 +  /* source dependencies and static content */
     3.9  
    3.10 -  sealed case class Node(
    3.11 +  sealed case class Session_Content(
    3.12      loaded_theories: Set[String],
    3.13      syntax: Outer_Syntax,
    3.14      sources: List[(Path, SHA1.Digest)])
    3.15  
    3.16 -  sealed case class Deps(deps: Map[String, Node])
    3.17 +  sealed case class Deps(deps: Map[String, Session_Content])
    3.18    {
    3.19      def is_empty: Boolean = deps.isEmpty
    3.20 -    def apply(name: String): Node = deps(name)
    3.21 +    def apply(name: String): Session_Content = deps(name)
    3.22      def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
    3.23    }
    3.24  
    3.25    def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
    3.26 -    Deps((Map.empty[String, Node] /: tree.topological_order)(
    3.27 +    Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
    3.28        { case (deps, (name, info)) =>
    3.29            val (preloaded, parent_syntax) =
    3.30              info.parent match {
    3.31 @@ -374,9 +374,17 @@
    3.32                    quote(name) + Position.str_of(info.pos))
    3.33              }
    3.34  
    3.35 -          deps + (name -> Node(loaded_theories, syntax, sources))
    3.36 +          deps + (name -> Session_Content(loaded_theories, syntax, sources))
    3.37        }))
    3.38  
    3.39 +  def session_content(session: String): Session_Content =
    3.40 +  {
    3.41 +    val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
    3.42 +    dependencies(false, tree)(session)
    3.43 +  }
    3.44 +
    3.45 +  def outer_syntax(session: String): Outer_Syntax = session_content(session).syntax
    3.46 +
    3.47  
    3.48    /* jobs */
    3.49  
    3.50 @@ -391,7 +399,7 @@
    3.51          browser_info + Path.explode("isabelle.gif"))
    3.52        File.write(browser_info + Path.explode("index.html"),
    3.53          File.read(Path.explode("~~/lib/html/library_index_header.template")) +
    3.54 -        File.read(Path.explode("~~/lib/html/library_index_content.template")) +
    3.55 +        File.read(Path.explode("~~/lib/html/library_index_Session_Content.template")) +
    3.56          File.read(Path.explode("~~/lib/html/library_index_footer.template")))
    3.57      }
    3.58  
    3.59 @@ -695,14 +703,5 @@
    3.60        }
    3.61      }
    3.62    }
    3.63 -
    3.64 -
    3.65 -  /* static outer syntax */
    3.66 -
    3.67 -  def outer_syntax(session: String): Outer_Syntax =
    3.68 -  {
    3.69 -    val (_, tree) = find_sessions(Options.init(), Nil).required(false, Nil, List(session))
    3.70 -    dependencies(false, tree)(session).syntax
    3.71 -  }
    3.72  }
    3.73  
     4.1 --- a/src/Pure/System/isabelle_process.ML	Tue Aug 07 16:34:15 2012 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Aug 07 17:08:22 2012 +0200
     4.3 @@ -183,7 +183,6 @@
     4.4      val channel = rendezvous ();
     4.5      val _ = setup_channels channel;
     4.6  
     4.7 -    val _ = Thy_Info.status ();
     4.8      val _ = Output.protocol_message Isabelle_Markup.ready "";
     4.9    in loop channel end));
    4.10  
     5.1 --- a/src/Pure/System/session.scala	Tue Aug 07 16:34:15 2012 +0200
     5.2 +++ b/src/Pure/System/session.scala	Tue Aug 07 17:08:22 2012 +0200
     5.3 @@ -37,7 +37,7 @@
     5.4  }
     5.5  
     5.6  
     5.7 -class Session(thy_load: Thy_Load = new Thy_Load())
     5.8 +class Session(val thy_load: Thy_Load = new Thy_Load())
     5.9  {
    5.10    /* global flags */
    5.11  
    5.12 @@ -354,9 +354,6 @@
    5.13          case Isabelle_Markup.Ready if output.is_protocol =>
    5.14              phase = Session.Ready
    5.15  
    5.16 -        case Isabelle_Markup.Loaded_Theory(name) if output.is_protocol =>
    5.17 -          thy_load.register_thy(name)
    5.18 -
    5.19          case Isabelle_Markup.Return_Code(rc) if output.is_exit =>
    5.20            if (rc == 0) phase = Session.Inactive
    5.21            else phase = Session.Failed
    5.22 @@ -380,7 +377,12 @@
    5.23          case Start(name, args) if prover.isEmpty =>
    5.24            if (phase == Session.Inactive || phase == Session.Failed) {
    5.25              phase = Session.Startup
    5.26 -            base_syntax = Build.outer_syntax(name)
    5.27 +
    5.28 +            // FIXME static init in main constructor
    5.29 +            val content = Build.session_content(name)
    5.30 +            thy_load.register_thys(content.loaded_theories)
    5.31 +            base_syntax = content.syntax
    5.32 +
    5.33              prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
    5.34            }
    5.35  
     6.1 --- a/src/Pure/Thy/thy_info.ML	Tue Aug 07 16:34:15 2012 +0200
     6.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Aug 07 17:08:22 2012 +0200
     6.3 @@ -10,7 +10,6 @@
     6.4    datatype action = Update | Remove
     6.5    val add_hook: (action -> string -> unit) -> unit
     6.6    val get_names: unit -> string list
     6.7 -  val status: unit -> unit
     6.8    val lookup_theory: string -> theory option
     6.9    val get_theory: string -> theory
    6.10    val is_finished: string -> bool
    6.11 @@ -88,10 +87,6 @@
    6.12  
    6.13  fun get_names () = Graph.topological_order (get_thys ());
    6.14  
    6.15 -fun status () =
    6.16 -  List.app (fn name => Output.protocol_message (Isabelle_Markup.loaded_theory name) "")
    6.17 -    (get_names ());
    6.18 -
    6.19  
    6.20  (* access thy *)
    6.21  
     7.1 --- a/src/Pure/Thy/thy_load.scala	Tue Aug 07 16:34:15 2012 +0200
     7.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Aug 07 17:08:22 2012 +0200
     7.3 @@ -26,8 +26,11 @@
     7.4  
     7.5    private var loaded_theories: Set[String] = preloaded
     7.6  
     7.7 -  def register_thy(thy_name: String): Unit =
     7.8 -    synchronized { loaded_theories += thy_name }
     7.9 +  def register_thy(name: String): Unit =
    7.10 +    synchronized { loaded_theories += name }
    7.11 +
    7.12 +  def register_thys(names: Set[String]): Unit =
    7.13 +    synchronized { loaded_theories ++= names }
    7.14  
    7.15    def is_loaded(thy_name: String): Boolean =
    7.16      synchronized { loaded_theories.contains(thy_name) }