--- 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
--- 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"
--- 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
- }
-}
--- 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,
--- /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
+ }
+}
--- 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)
--- 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)
--- 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)