src/Tools/jEdit/src/jedit_sessions.scala
author wenzelm
Thu Nov 02 10:16:22 2017 +0100 (17 months ago)
changeset 66987 352b23c97ac8
parent 66979 58b166fd8447
child 66988 7f8c1dd7576a
permissions -rw-r--r--
support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
wenzelm@62973
     1
/*  Title:      Tools/jEdit/src/jedit_sessions.scala
wenzelm@49246
     2
    Author:     Makarius
wenzelm@49246
     3
wenzelm@65256
     4
Isabelle/jEdit session information, based on implicit process environment
wenzelm@65256
     5
and explicit options.
wenzelm@49246
     6
*/
wenzelm@49246
     7
wenzelm@49246
     8
package isabelle.jedit
wenzelm@49246
     9
wenzelm@49246
    10
wenzelm@49246
    11
import isabelle._
wenzelm@49246
    12
wenzelm@49246
    13
import scala.swing.ComboBox
wenzelm@49246
    14
import scala.swing.event.SelectionChanged
wenzelm@49246
    15
wenzelm@49246
    16
wenzelm@62973
    17
object JEdit_Sessions
wenzelm@49246
    18
{
wenzelm@66973
    19
  /* session options */
wenzelm@62972
    20
wenzelm@65256
    21
  def session_options(options: Options): Options =
wenzelm@63986
    22
    Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
wenzelm@65256
    23
      case "" => options
wenzelm@66973
    24
      case s => options.string.update("ML_process_policy", s)
wenzelm@63986
    25
    }
wenzelm@63986
    26
wenzelm@66973
    27
  def session_dirs(): List[Path] =
wenzelm@66973
    28
    Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
wenzelm@66973
    29
wenzelm@66973
    30
  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
wenzelm@66973
    31
wenzelm@66973
    32
wenzelm@66973
    33
  /* raw logic info */
wenzelm@66973
    34
wenzelm@66973
    35
  private val jedit_logic_option = "jedit_logic"
wenzelm@66973
    36
wenzelm@66973
    37
  def logic_name(options: Options): String =
wenzelm@66973
    38
    Isabelle_System.default_logic(
wenzelm@66973
    39
      Isabelle_System.getenv("JEDIT_LOGIC"),
wenzelm@66973
    40
      options.string(jedit_logic_option))
wenzelm@64602
    41
wenzelm@66987
    42
  def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
wenzelm@66973
    43
  def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true"
wenzelm@66973
    44
  def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
wenzelm@66973
    45
wenzelm@66973
    46
  def logic_info(options: Options): Option[Sessions.Info] =
wenzelm@66973
    47
    try { Sessions.load(session_options(options), dirs = session_dirs()).get(logic_name(options)) }
wenzelm@66973
    48
    catch { case ERROR(_) => None }
wenzelm@64602
    49
wenzelm@66973
    50
  def logic_root(options: Options): Position.T =
wenzelm@66973
    51
    if (Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true") {
wenzelm@66973
    52
      logic_info(options).map(_.pos) getOrElse Position.none
wenzelm@66973
    53
    }
wenzelm@66973
    54
    else Position.none
wenzelm@66973
    55
wenzelm@66973
    56
wenzelm@66979
    57
  /* logic selector */
wenzelm@66979
    58
wenzelm@66979
    59
  private class Logic_Entry(val name: String, val description: String)
wenzelm@66979
    60
  {
wenzelm@66979
    61
    override def toString: String = description
wenzelm@66979
    62
  }
wenzelm@66979
    63
wenzelm@66979
    64
  def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component =
wenzelm@66979
    65
  {
wenzelm@66979
    66
    GUI_Thread.require {}
wenzelm@66979
    67
wenzelm@66979
    68
    val session_list =
wenzelm@66979
    69
    {
wenzelm@66979
    70
      val sessions = Sessions.load(options.value, dirs = session_dirs())
wenzelm@66979
    71
      val (main_sessions, other_sessions) =
wenzelm@66979
    72
        sessions.imports_topological_order.partition(info => info.groups.contains("main"))
wenzelm@66979
    73
      main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
wenzelm@66979
    74
    }
wenzelm@66979
    75
wenzelm@66979
    76
    val entries =
wenzelm@66979
    77
      new Logic_Entry("", "default (" + logic_name(options.value) + ")") ::
wenzelm@66979
    78
        session_list.map(name => new Logic_Entry(name, name))
wenzelm@66979
    79
wenzelm@66979
    80
    val component = new ComboBox(entries) with Option_Component {
wenzelm@66979
    81
      name = jedit_logic_option
wenzelm@66979
    82
      val title = "Logic"
wenzelm@66979
    83
      def load: Unit =
wenzelm@66979
    84
      {
wenzelm@66979
    85
        val logic = options.string(jedit_logic_option)
wenzelm@66979
    86
        entries.find(_.name == logic) match {
wenzelm@66979
    87
          case Some(entry) => selection.item = entry
wenzelm@66979
    88
          case None =>
wenzelm@66979
    89
        }
wenzelm@66979
    90
      }
wenzelm@66979
    91
      def save: Unit = options.string(jedit_logic_option) = selection.item.name
wenzelm@66979
    92
    }
wenzelm@66979
    93
wenzelm@66979
    94
    component.load()
wenzelm@66979
    95
    if (autosave) {
wenzelm@66979
    96
      component.listenTo(component.selection)
wenzelm@66979
    97
      component.reactions += { case SelectionChanged(_) => component.save() }
wenzelm@66979
    98
    }
wenzelm@66979
    99
    component.tooltip = "Logic session name (change requires restart)"
wenzelm@66979
   100
    component
wenzelm@66979
   101
  }
wenzelm@66979
   102
wenzelm@66979
   103
wenzelm@66979
   104
  /* session build process */
wenzelm@64602
   105
wenzelm@66963
   106
  def session_base_info(options: Options): Sessions.Base_Info =
wenzelm@66976
   107
    Sessions.base_info(options,
wenzelm@66987
   108
      session =
wenzelm@66987
   109
        if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
wenzelm@66987
   110
        else logic_name(options),
wenzelm@66973
   111
      dirs = JEdit_Sessions.session_dirs(),
wenzelm@66987
   112
      all_known = !logic_focus,
wenzelm@66987
   113
      focus_session = logic_focus,
wenzelm@66973
   114
      required_session = logic_base)
wenzelm@65571
   115
wenzelm@65256
   116
  def session_build(
wenzelm@65256
   117
    options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
wenzelm@62972
   118
  {
wenzelm@62972
   119
    val mode = session_build_mode()
wenzelm@62972
   120
wenzelm@65256
   121
    Build.build(options = session_options(options), progress = progress,
wenzelm@62972
   122
      build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
wenzelm@66973
   123
      dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
wenzelm@66973
   124
      sessions = List(PIDE.resources.session_name)).rc
wenzelm@62972
   125
  }
wenzelm@62972
   126
wenzelm@65256
   127
  def session_start(options: Options)
wenzelm@62972
   128
  {
wenzelm@65256
   129
    Isabelle_Process.start(PIDE.session, session_options(options),
wenzelm@66973
   130
      sessions = Some(PIDE.resources.session_base_info.sessions),
wenzelm@66973
   131
      logic = PIDE.resources.session_name,
wenzelm@65226
   132
      store = Sessions.store(session_build_mode() == "system"),
wenzelm@66973
   133
      modes =
wenzelm@66973
   134
        (space_explode(',', options.string("jedit_print_mode")) :::
wenzelm@66973
   135
         space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
wenzelm@65226
   136
      phase_changed = PIDE.plugin.session_phase_changed)
wenzelm@62972
   137
  }
wenzelm@49246
   138
}