tuned;
authorwenzelm
Wed Nov 01 17:07:43 2017 +0100 (19 months ago)
changeset 6697958b166fd8447
parent 66978 0525320d8774
child 66980 8947cf58cb86
tuned;
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 01 17:03:32 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Wed Nov 01 17:07:43 2017 +0100
     1.3 @@ -53,7 +53,54 @@
     1.4      else Position.none
     1.5  
     1.6  
     1.7 -  /* session base info */
     1.8 +  /* logic selector */
     1.9 +
    1.10 +  private class Logic_Entry(val name: String, val description: String)
    1.11 +  {
    1.12 +    override def toString: String = description
    1.13 +  }
    1.14 +
    1.15 +  def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component =
    1.16 +  {
    1.17 +    GUI_Thread.require {}
    1.18 +
    1.19 +    val session_list =
    1.20 +    {
    1.21 +      val sessions = Sessions.load(options.value, dirs = session_dirs())
    1.22 +      val (main_sessions, other_sessions) =
    1.23 +        sessions.imports_topological_order.partition(info => info.groups.contains("main"))
    1.24 +      main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
    1.25 +    }
    1.26 +
    1.27 +    val entries =
    1.28 +      new Logic_Entry("", "default (" + logic_name(options.value) + ")") ::
    1.29 +        session_list.map(name => new Logic_Entry(name, name))
    1.30 +
    1.31 +    val component = new ComboBox(entries) with Option_Component {
    1.32 +      name = jedit_logic_option
    1.33 +      val title = "Logic"
    1.34 +      def load: Unit =
    1.35 +      {
    1.36 +        val logic = options.string(jedit_logic_option)
    1.37 +        entries.find(_.name == logic) match {
    1.38 +          case Some(entry) => selection.item = entry
    1.39 +          case None =>
    1.40 +        }
    1.41 +      }
    1.42 +      def save: Unit = options.string(jedit_logic_option) = selection.item.name
    1.43 +    }
    1.44 +
    1.45 +    component.load()
    1.46 +    if (autosave) {
    1.47 +      component.listenTo(component.selection)
    1.48 +      component.reactions += { case SelectionChanged(_) => component.save() }
    1.49 +    }
    1.50 +    component.tooltip = "Logic session name (change requires restart)"
    1.51 +    component
    1.52 +  }
    1.53 +
    1.54 +
    1.55 +  /* session build process */
    1.56  
    1.57    def session_base_info(options: Options): Sessions.Base_Info =
    1.58    {
    1.59 @@ -88,51 +135,4 @@
    1.60           space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
    1.61        phase_changed = PIDE.plugin.session_phase_changed)
    1.62    }
    1.63 -
    1.64 -  def session_list(options: Options): List[String] =
    1.65 -  {
    1.66 -    val sessions = Sessions.load(options, dirs = session_dirs())
    1.67 -    val (main_sessions, other_sessions) =
    1.68 -      sessions.imports_topological_order.partition(info => info.groups.contains("main"))
    1.69 -    main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
    1.70 -  }
    1.71 -
    1.72 -
    1.73 -  /* logic selector */
    1.74 -
    1.75 -  private class Logic_Entry(val name: String, val description: String)
    1.76 -  {
    1.77 -    override def toString: String = description
    1.78 -  }
    1.79 -
    1.80 -  def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component =
    1.81 -  {
    1.82 -    GUI_Thread.require {}
    1.83 -
    1.84 -    val entries =
    1.85 -      new Logic_Entry("", "default (" + logic_name(options.value) + ")") ::
    1.86 -        session_list(options.value).map(name => new Logic_Entry(name, name))
    1.87 -
    1.88 -    val component = new ComboBox(entries) with Option_Component {
    1.89 -      name = jedit_logic_option
    1.90 -      val title = "Logic"
    1.91 -      def load: Unit =
    1.92 -      {
    1.93 -        val logic = options.string(jedit_logic_option)
    1.94 -        entries.find(_.name == logic) match {
    1.95 -          case Some(entry) => selection.item = entry
    1.96 -          case None =>
    1.97 -        }
    1.98 -      }
    1.99 -      def save: Unit = options.string(jedit_logic_option) = selection.item.name
   1.100 -    }
   1.101 -
   1.102 -    component.load()
   1.103 -    if (autosave) {
   1.104 -      component.listenTo(component.selection)
   1.105 -      component.reactions += { case SelectionChanged(_) => component.save() }
   1.106 -    }
   1.107 -    component.tooltip = "Logic session name (change requires restart)"
   1.108 -    component
   1.109 -  }
   1.110  }