src/Tools/jEdit/src/jedit_sessions.scala
author wenzelm
Tue Nov 07 15:45:33 2017 +0100 (17 months ago)
changeset 67023 e27e05d6f2a7
parent 66989 25665e7775b7
child 67024 72d37a2e9cca
permissions -rw-r--r--
tuned signature;
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@66988
    42
  def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
wenzelm@66987
    43
  def logic_focus: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_FOCUS") == "true"
wenzelm@66973
    44
  def logic_base: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_BASE") == "true"
wenzelm@66973
    45
  def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
wenzelm@66973
    46
wenzelm@66973
    47
  def logic_info(options: Options): Option[Sessions.Info] =
wenzelm@66973
    48
    try { Sessions.load(session_options(options), dirs = session_dirs()).get(logic_name(options)) }
wenzelm@66973
    49
    catch { case ERROR(_) => None }
wenzelm@64602
    50
wenzelm@66973
    51
  def logic_root(options: Options): Position.T =
wenzelm@66973
    52
    if (Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true") {
wenzelm@66973
    53
      logic_info(options).map(_.pos) getOrElse Position.none
wenzelm@66973
    54
    }
wenzelm@66973
    55
    else Position.none
wenzelm@66973
    56
wenzelm@66973
    57
wenzelm@66979
    58
  /* logic selector */
wenzelm@66979
    59
wenzelm@66979
    60
  private class Logic_Entry(val name: String, val description: String)
wenzelm@66979
    61
  {
wenzelm@66979
    62
    override def toString: String = description
wenzelm@66979
    63
  }
wenzelm@66979
    64
wenzelm@66979
    65
  def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component =
wenzelm@66979
    66
  {
wenzelm@66979
    67
    GUI_Thread.require {}
wenzelm@66979
    68
wenzelm@66979
    69
    val session_list =
wenzelm@66979
    70
    {
wenzelm@67023
    71
      val sessions_structure = Sessions.load(options.value, dirs = session_dirs())
wenzelm@66979
    72
      val (main_sessions, other_sessions) =
wenzelm@67023
    73
        sessions_structure.imports_topological_order.
wenzelm@67023
    74
          partition(name => sessions_structure(name).groups.contains("main"))
wenzelm@67023
    75
      main_sessions.sorted ::: other_sessions.sorted
wenzelm@66979
    76
    }
wenzelm@66979
    77
wenzelm@66979
    78
    val entries =
wenzelm@66979
    79
      new Logic_Entry("", "default (" + logic_name(options.value) + ")") ::
wenzelm@66979
    80
        session_list.map(name => new Logic_Entry(name, name))
wenzelm@66979
    81
wenzelm@66979
    82
    val component = new ComboBox(entries) with Option_Component {
wenzelm@66979
    83
      name = jedit_logic_option
wenzelm@66979
    84
      val title = "Logic"
wenzelm@66979
    85
      def load: Unit =
wenzelm@66979
    86
      {
wenzelm@66979
    87
        val logic = options.string(jedit_logic_option)
wenzelm@66979
    88
        entries.find(_.name == logic) match {
wenzelm@66979
    89
          case Some(entry) => selection.item = entry
wenzelm@66979
    90
          case None =>
wenzelm@66979
    91
        }
wenzelm@66979
    92
      }
wenzelm@66979
    93
      def save: Unit = options.string(jedit_logic_option) = selection.item.name
wenzelm@66979
    94
    }
wenzelm@66979
    95
wenzelm@66979
    96
    component.load()
wenzelm@66979
    97
    if (autosave) {
wenzelm@66979
    98
      component.listenTo(component.selection)
wenzelm@66979
    99
      component.reactions += { case SelectionChanged(_) => component.save() }
wenzelm@66979
   100
    }
wenzelm@66979
   101
    component.tooltip = "Logic session name (change requires restart)"
wenzelm@66979
   102
    component
wenzelm@66979
   103
  }
wenzelm@66979
   104
wenzelm@66979
   105
wenzelm@66979
   106
  /* session build process */
wenzelm@64602
   107
wenzelm@66963
   108
  def session_base_info(options: Options): Sessions.Base_Info =
wenzelm@66976
   109
    Sessions.base_info(options,
wenzelm@66989
   110
      dirs = JEdit_Sessions.session_dirs(),
wenzelm@66987
   111
      session =
wenzelm@66987
   112
        if (logic_parent) logic_info(options).flatMap(_.parent) getOrElse logic_name(options)
wenzelm@66987
   113
        else logic_name(options),
wenzelm@66988
   114
      ancestor_session = logic_ancestor,
wenzelm@66987
   115
      all_known = !logic_focus,
wenzelm@66987
   116
      focus_session = logic_focus,
wenzelm@66973
   117
      required_session = logic_base)
wenzelm@65571
   118
wenzelm@65256
   119
  def session_build(
wenzelm@65256
   120
    options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
wenzelm@62972
   121
  {
wenzelm@62972
   122
    val mode = session_build_mode()
wenzelm@62972
   123
wenzelm@65256
   124
    Build.build(options = session_options(options), progress = progress,
wenzelm@62972
   125
      build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
wenzelm@66973
   126
      dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
wenzelm@66973
   127
      sessions = List(PIDE.resources.session_name)).rc
wenzelm@62972
   128
  }
wenzelm@62972
   129
wenzelm@65256
   130
  def session_start(options: Options)
wenzelm@62972
   131
  {
wenzelm@65256
   132
    Isabelle_Process.start(PIDE.session, session_options(options),
wenzelm@66973
   133
      sessions = Some(PIDE.resources.session_base_info.sessions),
wenzelm@66973
   134
      logic = PIDE.resources.session_name,
wenzelm@65226
   135
      store = Sessions.store(session_build_mode() == "system"),
wenzelm@66973
   136
      modes =
wenzelm@66973
   137
        (space_explode(',', options.string("jedit_print_mode")) :::
wenzelm@66973
   138
         space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse,
wenzelm@65226
   139
      phase_changed = PIDE.plugin.session_phase_changed)
wenzelm@62972
   140
  }
wenzelm@49246
   141
}