# HG changeset patch
# User wenzelm
# Date 1460628518 -7200
# Node ID 744266e32612b383106e2a423d30a6dc904c8908
# Parent  0eedd78c2b475a615b546b621025018c65a1b514
clarified modules;

diff -r 0eedd78c2b47 -r 744266e32612 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 14 12:00:29 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 14 12:08:38 2016 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Thy/sessions.scala
     Author:     Makarius
 
-Session information.
+Isabelle session information.
 */
 
 package isabelle
diff -r 0eedd78c2b47 -r 744266e32612 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Apr 14 12:00:29 2016 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Apr 14 12:08:38 2016 +0200
@@ -35,13 +35,13 @@
   "src/info_dockable.scala"
   "src/isabelle.scala"
   "src/isabelle_encoding.scala"
-  "src/isabelle_logic.scala"
   "src/isabelle_options.scala"
   "src/isabelle_sidekick.scala"
   "src/jedit_editor.scala"
   "src/jedit_lib.scala"
   "src/jedit_options.scala"
   "src/jedit_resources.scala"
+  "src/jedit_sessions.scala"
   "src/monitor_dockable.scala"
   "src/output_dockable.scala"
   "src/pide_docking_framework.scala"
diff -r 0eedd78c2b47 -r 744266e32612 src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Thu Apr 14 12:00:29 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-/*  Title:      Tools/jEdit/src/isabelle_logic.scala
-    Author:     Makarius
-
-Isabelle logic session.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import scala.swing.ComboBox
-import scala.swing.event.SelectionChanged
-
-
-object Isabelle_Logic
-{
-  /* session info */
-
-  private val option_name = "jedit_logic"
-
-  def session_name(): String =
-    Isabelle_System.default_logic(
-      Isabelle_System.getenv("JEDIT_LOGIC"),
-      PIDE.options.string(option_name))
-
-  def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
-
-  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
-
-  def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
-  {
-    val mode = session_build_mode()
-
-    Build.build(options = PIDE.options.value, progress = progress,
-      build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
-      dirs = session_dirs(), sessions = List(session_name())).rc
-  }
-
-  def session_start()
-  {
-    val modes =
-      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
-       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
-    PIDE.session.start(receiver =>
-      Isabelle_Process(PIDE.options.value, logic = session_name(), dirs = session_dirs(),
-        modes = modes, receiver = receiver,
-        store = Sessions.store(session_build_mode() == "system")))
-  }
-
-  def session_list(): List[String] =
-  {
-    val session_tree = Sessions.load(PIDE.options.value, dirs = session_dirs())
-    val (main_sessions, other_sessions) =
-      session_tree.topological_order.partition(p => p._2.groups.contains("main"))
-    main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
-  }
-
-  def session_content(inlined_files: Boolean): Build.Session_Content =
-  {
-    val content =
-      Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
-    content.copy(known_theories =
-      content.known_theories.mapValues(name => name.map(File.platform_path(_))))
-  }
-
-
-  /* logic selector */
-
-  private class Logic_Entry(val name: String, val description: String)
-  {
-    override def toString: String = description
-  }
-
-  def logic_selector(autosave: Boolean): Option_Component =
-  {
-    GUI_Thread.require {}
-
-    val entries =
-      new Logic_Entry("", "default (" + session_name() + ")") ::
-        Isabelle_Logic.session_list().map(name => new Logic_Entry(name, name))
-
-    val component = new ComboBox(entries) with Option_Component {
-      name = option_name
-      val title = "Logic"
-      def load: Unit =
-      {
-        val logic = PIDE.options.string(option_name)
-        entries.find(_.name == logic) match {
-          case Some(entry) => selection.item = entry
-          case None =>
-        }
-      }
-      def save: Unit = PIDE.options.string(option_name) = selection.item.name
-    }
-
-    component.load()
-    if (autosave) {
-      component.listenTo(component.selection)
-      component.reactions += { case SelectionChanged(_) => component.save() }
-    }
-    component.tooltip = "Logic session name (change requires restart)"
-    component
-  }
-}
diff -r 0eedd78c2b47 -r 744266e32612 src/Tools/jEdit/src/isabelle_options.scala
--- a/src/Tools/jEdit/src/isabelle_options.scala	Thu Apr 14 12:00:29 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Apr 14 12:08:38 2016 +0200
@@ -42,7 +42,7 @@
   val options = PIDE.options
 
   private val predefined =
-    List(Isabelle_Logic.logic_selector(false), Spell_Checker.dictionaries_selector())
+    List(JEdit_Sessions.logic_selector(false), Spell_Checker.dictionaries_selector())
 
   protected val components =
     options.make_components(predefined,
diff -r 0eedd78c2b47 -r 744266e32612 src/Tools/jEdit/src/jedit_sessions.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Thu Apr 14 12:08:38 2016 +0200
@@ -0,0 +1,105 @@
+/*  Title:      Tools/jEdit/src/jedit_sessions.scala
+    Author:     Makarius
+
+Isabelle/jEdit session information.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.swing.ComboBox
+import scala.swing.event.SelectionChanged
+
+
+object JEdit_Sessions
+{
+  /* session info */
+
+  private val option_name = "jedit_logic"
+
+  def session_name(): String =
+    Isabelle_System.default_logic(
+      Isabelle_System.getenv("JEDIT_LOGIC"),
+      PIDE.options.string(option_name))
+
+  def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+
+  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
+
+  def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
+  {
+    val mode = session_build_mode()
+
+    Build.build(options = PIDE.options.value, progress = progress,
+      build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
+      dirs = session_dirs(), sessions = List(session_name())).rc
+  }
+
+  def session_start()
+  {
+    val modes =
+      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
+       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
+    PIDE.session.start(receiver =>
+      Isabelle_Process(PIDE.options.value, logic = session_name(), dirs = session_dirs(),
+        modes = modes, receiver = receiver,
+        store = Sessions.store(session_build_mode() == "system")))
+  }
+
+  def session_list(): List[String] =
+  {
+    val session_tree = Sessions.load(PIDE.options.value, dirs = session_dirs())
+    val (main_sessions, other_sessions) =
+      session_tree.topological_order.partition(p => p._2.groups.contains("main"))
+    main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
+  }
+
+  def session_content(inlined_files: Boolean): Build.Session_Content =
+  {
+    val content =
+      Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
+    content.copy(known_theories =
+      content.known_theories.mapValues(name => name.map(File.platform_path(_))))
+  }
+
+
+  /* logic selector */
+
+  private class Logic_Entry(val name: String, val description: String)
+  {
+    override def toString: String = description
+  }
+
+  def logic_selector(autosave: Boolean): Option_Component =
+  {
+    GUI_Thread.require {}
+
+    val entries =
+      new Logic_Entry("", "default (" + session_name() + ")") ::
+        JEdit_Sessions.session_list().map(name => new Logic_Entry(name, name))
+
+    val component = new ComboBox(entries) with Option_Component {
+      name = option_name
+      val title = "Logic"
+      def load: Unit =
+      {
+        val logic = PIDE.options.string(option_name)
+        entries.find(_.name == logic) match {
+          case Some(entry) => selection.item = entry
+          case None =>
+        }
+      }
+      def save: Unit = PIDE.options.string(option_name) = selection.item.name
+    }
+
+    component.load()
+    if (autosave) {
+      component.listenTo(component.selection)
+      component.reactions += { case SelectionChanged(_) => component.save() }
+    }
+    component.tooltip = "Logic session name (change requires restart)"
+    component
+  }
+}
diff -r 0eedd78c2b47 -r 744266e32612 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Apr 14 12:00:29 2016 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Apr 14 12:08:38 2016 +0200
@@ -410,7 +410,7 @@
 
       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
 
-      val content = Isabelle_Logic.session_content(false)
+      val content = JEdit_Sessions.session_content(false)
       val resources =
         new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax)
 
diff -r 0eedd78c2b47 -r 744266e32612 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Thu Apr 14 12:00:29 2016 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Thu Apr 14 12:08:38 2016 +0200
@@ -26,8 +26,8 @@
     GUI_Thread.require {}
 
     try {
-      if (Isabelle_Logic.session_build_mode() == "none" ||
-          Isabelle_Logic.session_build(no_build = true) == 0) Isabelle_Logic.session_start()
+      if (JEdit_Sessions.session_build_mode() == "none" ||
+          JEdit_Sessions.session_build(no_build = true) == 0) JEdit_Sessions.session_start()
       else new Dialog(view)
     }
     catch {
@@ -162,10 +162,10 @@
     setVisible(true)
 
     Standard_Thread.fork("session_build") {
-      progress.echo("Build started for Isabelle/" + Isabelle_Logic.session_name() + " ...")
+      progress.echo("Build started for Isabelle/" + JEdit_Sessions.session_name() + " ...")
 
       val (out, rc) =
-        try { ("", Isabelle_Logic.session_build(progress = progress)) }
+        try { ("", JEdit_Sessions.session_build(progress = progress)) }
         catch {
           case exn: Throwable =>
             (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
@@ -173,7 +173,7 @@
 
       progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))
 
-      if (rc == 0) Isabelle_Logic.session_start()
+      if (rc == 0) JEdit_Sessions.session_start()
       else progress.echo("Session build failed -- prover process remains inactive!")
 
       return_code(rc)
diff -r 0eedd78c2b47 -r 744266e32612 src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Thu Apr 14 12:00:29 2016 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Thu Apr 14 12:08:38 2016 +0200
@@ -80,7 +80,7 @@
   private val continuous_checking = new Isabelle.Continuous_Checking
   continuous_checking.focusable = false
 
-  private val logic = Isabelle_Logic.logic_selector(true)
+  private val logic = JEdit_Sessions.logic_selector(true)
 
   private val controls =
     new Wrap_Panel(Wrap_Panel.Alignment.Right)(continuous_checking, session_phase, logic)