clarified initialization of Thy_Load, Thy_Info, Session;
authorwenzelm
Tue Aug 21 12:15:25 2012 +0200 (2012-08-21)
changeset 488704accee106f0f
parent 48869 4371a8d029f2
child 48871 c82720f054c3
clarified initialization of Thy_Load, Thy_Info, Session;
src/Pure/Isar/outer_syntax.scala
src/Pure/System/build.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_load.scala
src/Tools/jEdit/src/jedit_thy_load.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 21 11:00:54 2012 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 21 12:15:25 2012 +0200
     1.3 @@ -35,7 +35,11 @@
     1.4    }
     1.5  
     1.6    val empty: Outer_Syntax = new Outer_Syntax()
     1.7 +
     1.8    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
     1.9 +
    1.10 +  def init_pure(): Outer_Syntax =
    1.11 +    init() + ("theory", Keyword.THY_BEGIN) + ("ML_file", Keyword.THY_LOAD)
    1.12  }
    1.13  
    1.14  final class Outer_Syntax private(
     2.1 --- a/src/Pure/System/build.scala	Tue Aug 21 11:00:54 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Tue Aug 21 12:15:25 2012 +0200
     2.3 @@ -333,20 +333,13 @@
     2.4        { case (deps, (name, info)) =>
     2.5            val (preloaded, parent_syntax, parent_errors) =
     2.6              info.parent match {
     2.7 +              case None =>
     2.8 +                (Set.empty[String], Outer_Syntax.init_pure(), Nil)
     2.9                case Some(parent_name) =>
    2.10                  val parent = deps(parent_name)
    2.11                  (parent.loaded_theories, parent.syntax, parent.errors)
    2.12 -              case None =>
    2.13 -                val init_syntax =
    2.14 -                  Outer_Syntax.init() +
    2.15 -                    // FIXME avoid hardwired stuff!?
    2.16 -                    ("theory", Keyword.THY_BEGIN) +
    2.17 -                    ("ML_file", Keyword.THY_LOAD) +
    2.18 -                    ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
    2.19 -                    ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
    2.20 -                (Set.empty[String], init_syntax, Nil)
    2.21              }
    2.22 -          val thy_info = new Thy_Info(new Thy_Load(preloaded))
    2.23 +          val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
    2.24  
    2.25            if (verbose) {
    2.26              val groups =
    2.27 @@ -361,7 +354,15 @@
    2.28                  map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
    2.29  
    2.30            val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
    2.31 -          val syntax = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
    2.32 +          val syntax0 = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
    2.33 +          val syntax =
    2.34 +            // FIXME avoid hardwired stuff!?
    2.35 +            // FIXME broken?!
    2.36 +            if (name == "Pure")
    2.37 +              syntax0 +
    2.38 +                ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
    2.39 +                ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
    2.40 +            else syntax0
    2.41  
    2.42            val all_files =
    2.43              thy_deps.map({ case (n, h) =>
     3.1 --- a/src/Pure/System/session.scala	Tue Aug 21 11:00:54 2012 +0200
     3.2 +++ b/src/Pure/System/session.scala	Tue Aug 21 12:15:25 2012 +0200
     3.3 @@ -37,7 +37,7 @@
     3.4  }
     3.5  
     3.6  
     3.7 -class Session(val thy_load: Thy_Load = new Thy_Load())
     3.8 +class Session(val thy_load: Thy_Load)
     3.9  {
    3.10    /* global flags */
    3.11  
    3.12 @@ -108,7 +108,7 @@
    3.13            val prev = previous.get_finished
    3.14            val (doc_edits, version) =
    3.15              Timing.timeit("Thy_Syntax.text_edits", timing) {
    3.16 -              Thy_Syntax.text_edits(base_syntax, prev, text_edits)
    3.17 +              Thy_Syntax.text_edits(thy_load.base_syntax, prev, text_edits)
    3.18              }
    3.19            version_result.fulfill(version)
    3.20            sender ! Change(doc_edits, prev, version)
    3.21 @@ -125,8 +125,6 @@
    3.22  
    3.23    /* global state */
    3.24  
    3.25 -  @volatile private var base_syntax = Outer_Syntax.init()
    3.26 -
    3.27    private val syslog = Volatile(Queue.empty[XML.Elem])
    3.28    def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
    3.29  
    3.30 @@ -145,7 +143,7 @@
    3.31    def recent_syntax(): Outer_Syntax =
    3.32    {
    3.33      val version = current_state().recent_finished.version.get_finished
    3.34 -    if (version.is_init) base_syntax
    3.35 +    if (version.is_init) thy_load.base_syntax
    3.36      else version.syntax
    3.37    }
    3.38    def get_recent_syntax(): Option[Outer_Syntax] =
    3.39 @@ -162,7 +160,7 @@
    3.40    def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
    3.41    {
    3.42      val header1 =
    3.43 -      if (thy_load.is_loaded(name.theory))
    3.44 +      if (thy_load.loaded_theories(name.theory))
    3.45          header.error("Attempt to update loaded theory " + quote(name.theory))
    3.46        else header
    3.47      (name, Document.Node.Deps(header1))
    3.48 @@ -171,7 +169,7 @@
    3.49  
    3.50    /* actor messages */
    3.51  
    3.52 -  private case class Start(dirs: List[Path], logic: String, args: List[String])
    3.53 +  private case class Start(args: List[String])
    3.54    private case object Cancel_Execution
    3.55    private case class Edit(edits: List[Document.Edit_Text])
    3.56    private case class Change(
    3.57 @@ -377,15 +375,9 @@
    3.58        receiveWithin(delay_commands_changed.flush_timeout) {
    3.59          case TIMEOUT => delay_commands_changed.flush()
    3.60  
    3.61 -        case Start(dirs, name, args) if prover.isEmpty =>
    3.62 +        case Start(args) if prover.isEmpty =>
    3.63            if (phase == Session.Inactive || phase == Session.Failed) {
    3.64              phase = Session.Startup
    3.65 -
    3.66 -            // FIXME static init in main constructor
    3.67 -            val content = Build.session_content(dirs, name).check_errors
    3.68 -            thy_load.register_thys(content.loaded_theories)
    3.69 -            base_syntax = content.syntax
    3.70 -
    3.71              prover = Some(new Isabelle_Process(receiver.invoke _, args) with Protocol)
    3.72            }
    3.73  
    3.74 @@ -440,8 +432,8 @@
    3.75  
    3.76    /* actions */
    3.77  
    3.78 -  def start(dirs: List[Path], name: String, args: List[String])
    3.79 -  { session_actor ! Start(dirs, name, args) }
    3.80 +  def start(args: List[String])
    3.81 +  { session_actor ! Start(args) }
    3.82  
    3.83    def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
    3.84  
     4.1 --- a/src/Pure/Thy/thy_info.scala	Tue Aug 21 11:00:54 2012 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Aug 21 12:15:25 2012 +0200
     4.3 @@ -36,7 +36,7 @@
     4.4    {
     4.5      val (deps, seen) = required
     4.6      if (seen(name)) required
     4.7 -    else if (thy_load.is_loaded(name.theory)) (deps, seen + name)
     4.8 +    else if (thy_load.loaded_theories(name.theory)) (deps, seen + name)
     4.9      else {
    4.10        try {
    4.11          if (initiators.contains(name)) error(cycle_msg(initiators))
     5.1 --- a/src/Pure/Thy/thy_load.scala	Tue Aug 21 11:00:54 2012 +0200
     5.2 +++ b/src/Pure/Thy/thy_load.scala	Tue Aug 21 12:15:25 2012 +0200
     5.3 @@ -20,22 +20,8 @@
     5.4  }
     5.5  
     5.6  
     5.7 -class Thy_Load(preloaded: Set[String] = Set.empty)
     5.8 +class Thy_Load(val loaded_theories: Set[String] = Set.empty, val base_syntax: Outer_Syntax)
     5.9  {
    5.10 -  /* loaded theories provided by prover */
    5.11 -
    5.12 -  private var loaded_theories: Set[String] = preloaded
    5.13 -
    5.14 -  def register_thy(name: String): Unit =
    5.15 -    synchronized { loaded_theories += name }
    5.16 -
    5.17 -  def register_thys(names: Set[String]): Unit =
    5.18 -    synchronized { loaded_theories ++= names }
    5.19 -
    5.20 -  def is_loaded(thy_name: String): Boolean =
    5.21 -    synchronized { loaded_theories.contains(thy_name) }
    5.22 -
    5.23 -
    5.24    /* file-system operations */
    5.25  
    5.26    def append(dir: String, source_path: Path): String =
    5.27 @@ -54,7 +40,7 @@
    5.28    private def import_name(dir: String, s: String): Document.Node.Name =
    5.29    {
    5.30      val theory = Thy_Header.base_name(s)
    5.31 -    if (is_loaded(theory)) Document.Node.Name(theory, "", theory)
    5.32 +    if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
    5.33      else {
    5.34        val path = Path.explode(s)
    5.35        val node = append(dir, Thy_Load.thy_path(path))
     6.1 --- a/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 21 11:00:54 2012 +0200
     6.2 +++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Aug 21 12:15:25 2012 +0200
     6.3 @@ -17,7 +17,8 @@
     6.4  import org.gjt.sp.jedit.View
     6.5  
     6.6  
     6.7 -class JEdit_Thy_Load extends Thy_Load()
     6.8 +class JEdit_Thy_Load(loaded_theories: Set[String] = Set.empty, base_syntax: Outer_Syntax)
     6.9 +  extends Thy_Load(loaded_theories, base_syntax)
    6.10  {
    6.11    override def append(dir: String, source_path: Path): String =
    6.12    {
     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 21 11:00:54 2012 +0200
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 21 12:15:25 2012 +0200
     7.3 @@ -37,8 +37,8 @@
     7.4    var plugin: Plugin = null
     7.5    var session: Session = null
     7.6  
     7.7 -  val thy_load = new JEdit_Thy_Load
     7.8 -  val thy_info = new Thy_Info(thy_load)
     7.9 +  def thy_load(): JEdit_Thy_Load =
    7.10 +    session.thy_load.asInstanceOf[JEdit_Thy_Load]
    7.11  
    7.12  
    7.13    /* properties */
    7.14 @@ -298,17 +298,22 @@
    7.15      component
    7.16    }
    7.17  
    7.18 -  def start_session()
    7.19 +  def session_args(): List[String] =
    7.20    {
    7.21 -    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    7.22      val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
    7.23      val logic = {
    7.24        val logic = Property("logic")
    7.25        if (logic != null && logic != "") logic
    7.26        else Isabelle.default_logic()
    7.27      }
    7.28 -    val name = Path.explode(logic).base.implode  // FIXME more robust session name
    7.29 -    session.start(dirs, name, modes ::: List(logic))
    7.30 +    modes ::: List(logic)
    7.31 +  }
    7.32 +
    7.33 +  def session_content(): Build.Session_Content =
    7.34 +  {
    7.35 +    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    7.36 +    val name = Path.explode(session_args().last).base.implode  // FIXME more robust
    7.37 +    Build.session_content(dirs, name).check_errors
    7.38    }
    7.39  
    7.40  
    7.41 @@ -359,8 +364,9 @@
    7.42            for (buffer <- buffers; model <- Isabelle.document_model(buffer))
    7.43              yield model.name
    7.44  
    7.45 +        val thy_info = new Thy_Info(Isabelle.thy_load)
    7.46          // FIXME avoid I/O in Swing thread!?!
    7.47 -        val files = Isabelle.thy_info.dependencies(thys).map(_._1.node).
    7.48 +        val files = thy_info.dependencies(thys).map(_._1.node).
    7.49            filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
    7.50  
    7.51          if (!files.isEmpty) {
    7.52 @@ -422,7 +428,7 @@
    7.53      message match {
    7.54        case msg: EditorStarted =>
    7.55          if (Isabelle.Boolean_Property("auto-start"))
    7.56 -          Isabelle.start_session()
    7.57 +          Isabelle.session.start(Isabelle.session_args())
    7.58  
    7.59        case msg: BufferUpdate
    7.60        if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
    7.61 @@ -459,12 +465,16 @@
    7.62    }
    7.63  
    7.64    override def start()
    7.65 -  {
    7.66 +  { // FIXME more robust error handling
    7.67      Isabelle.plugin = this
    7.68      Isabelle.setup_tooltips()
    7.69      Isabelle_System.init()
    7.70      Isabelle_System.install_fonts()
    7.71 -    Isabelle.session = new Session(Isabelle.thy_load)
    7.72 +
    7.73 +    val content = Isabelle.session_content()
    7.74 +    val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
    7.75 +    Isabelle.session = new Session(thy_load)
    7.76 +
    7.77      SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
    7.78      if (ModeProvider.instance.isInstanceOf[ModeProvider])
    7.79        ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
     8.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Tue Aug 21 11:00:54 2012 +0200
     8.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Aug 21 12:15:25 2012 +0200
     8.3 @@ -134,7 +134,7 @@
     8.4          }
     8.5        val nodes_status1 =
     8.6          (nodes_status /: iterator)({ case (status, (name, node)) =>
     8.7 -            if (Isabelle.thy_load.is_loaded(name.theory)) status
     8.8 +            if (Isabelle.thy_load.loaded_theories(name.theory)) status
     8.9              else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
    8.10  
    8.11        if (nodes_status != nodes_status1) {