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