# HG changeset patch
# User wenzelm
# Date 1354742715 -3600
# Node ID b1cb764187607f6ff963237d3016ecefd64ef0a4
# Parent  a8b0d3729a691f078e3fbe77e1834a092869d8b6
select logic session names, not paths;

diff -r a8b0d3729a69 -r b1cb76418760 src/Tools/jEdit/src/isabelle_logic.scala
--- a/src/Tools/jEdit/src/isabelle_logic.scala	Wed Dec 05 21:13:50 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala	Wed Dec 05 22:25:15 2012 +0100
@@ -35,7 +35,7 @@
 
     val entries =
       new Logic_Entry("", "default (" + default_logic() + ")") ::
-        Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
+        Isabelle_Logic.session_list().map(name => new Logic_Entry(name, name))
 
     val component = new ComboBox(entries) with Option_Component {
       name = option_name
@@ -56,7 +56,7 @@
       component.listenTo(component.selection)
       component.reactions += { case SelectionChanged(_) => component.save() }
     }
-    component.tooltip = PIDE.options.value.check_name(option_name).print_default
+    component.tooltip = "Logic session name (change requires restart)"
     component
   }
 
@@ -71,9 +71,17 @@
     modes ::: List(logic)
   }
 
+  def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+
+  def session_list(): List[String] =
+  {
+    val dirs = session_dirs().map((false, _))
+    Build.find_sessions(PIDE.options.value, dirs).topological_order.map(_._1).sorted
+  }
+
   def session_content(inlined_files: Boolean): Build.Session_Content =
   {
-    val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+    val dirs = session_dirs()
     val name = session_args().last
     Build.session_content(inlined_files, dirs, name).check_errors
   }