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