src/Tools/jEdit/src/jedit_sessions.scala
author wenzelm
Wed, 15 Mar 2017 11:04:46 +0100
changeset 65254 3075aa3b40bf
parent 65252 8b776d12f6c0
child 65256 c3d6dd17d626
permissions -rw-r--r--
clarified fall-back base, e.g. relevant for "isabelle jedit -l BAD";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62973
744266e32612 clarified modules;
wenzelm
parents: 62972
diff changeset
     1
/*  Title:      Tools/jEdit/src/jedit_sessions.scala
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
     3
62973
744266e32612 clarified modules;
wenzelm
parents: 62972
diff changeset
     4
Isabelle/jEdit session information.
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
     5
*/
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
     6
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
     8
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
     9
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    10
import isabelle._
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    11
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    12
import scala.swing.ComboBox
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    13
import scala.swing.event.SelectionChanged
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    14
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    15
62973
744266e32612 clarified modules;
wenzelm
parents: 62972
diff changeset
    16
object JEdit_Sessions
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    17
{
62972
wenzelm
parents: 62754
diff changeset
    18
  /* session info */
wenzelm
parents: 62754
diff changeset
    19
50403
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50380
diff changeset
    20
  private val option_name = "jedit_logic"
87868964733c more uniform default logic, using settings, options, args etc.;
wenzelm
parents: 50380
diff changeset
    21
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    22
  sealed case class Info(name: String, open_root: Position.T)
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    23
62972
wenzelm
parents: 62754
diff changeset
    24
  def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
wenzelm
parents: 62754
diff changeset
    25
63986
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62974
diff changeset
    26
  def session_options(): Options =
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62974
diff changeset
    27
    Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62974
diff changeset
    28
      case "" => PIDE.options.value
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62974
diff changeset
    29
      case s => PIDE.options.value.string("ML_process_policy") = s
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62974
diff changeset
    30
    }
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62974
diff changeset
    31
64602
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    32
  def session_info(): Info =
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    33
  {
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    34
    val logic =
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    35
      Isabelle_System.default_logic(
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    36
        Isabelle_System.getenv("JEDIT_LOGIC"),
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    37
        PIDE.options.string(option_name))
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    38
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    39
    (for {
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    40
      tree <-
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    41
        try { Some(Sessions.load(session_options(), dirs = session_dirs())) }
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    42
        catch { case ERROR(_) => None }
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    43
      info <- tree.lift(logic)
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    44
      parent <- info.parent
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    45
      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    46
    } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    47
  }
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    48
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    49
  def session_name(): String = session_info().name
8edca3465758 added isabelle jedit -R;
wenzelm
parents: 63986
diff changeset
    50
62972
wenzelm
parents: 62754
diff changeset
    51
  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
wenzelm
parents: 62754
diff changeset
    52
64909
8007f10195af tuned signature;
wenzelm
parents: 64856
diff changeset
    53
  def session_build(progress: Progress = No_Progress, no_build: Boolean = false): Int =
62972
wenzelm
parents: 62754
diff changeset
    54
  {
wenzelm
parents: 62754
diff changeset
    55
    val mode = session_build_mode()
wenzelm
parents: 62754
diff changeset
    56
63986
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62974
diff changeset
    57
    Build.build(options = session_options(), progress = progress,
62972
wenzelm
parents: 62754
diff changeset
    58
      build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
wenzelm
parents: 62754
diff changeset
    59
      dirs = session_dirs(), sessions = List(session_name())).rc
wenzelm
parents: 62754
diff changeset
    60
  }
wenzelm
parents: 62754
diff changeset
    61
wenzelm
parents: 62754
diff changeset
    62
  def session_start()
wenzelm
parents: 62754
diff changeset
    63
  {
wenzelm
parents: 62754
diff changeset
    64
    val modes =
wenzelm
parents: 62754
diff changeset
    65
      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
wenzelm
parents: 62754
diff changeset
    66
       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
63986
c7a4b03727ae options for process policy, notably for multiprocessor machines;
wenzelm
parents: 62974
diff changeset
    67
65216
060a8a1f2dec tuned signature;
wenzelm
parents: 65210
diff changeset
    68
    Isabelle_Process.start(PIDE.session, session_options(),
060a8a1f2dec tuned signature;
wenzelm
parents: 65210
diff changeset
    69
      logic = session_name(), dirs = session_dirs(), modes = modes,
65226
wenzelm
parents: 65216
diff changeset
    70
      store = Sessions.store(session_build_mode() == "system"),
wenzelm
parents: 65216
diff changeset
    71
      phase_changed = PIDE.plugin.session_phase_changed)
62972
wenzelm
parents: 62754
diff changeset
    72
  }
wenzelm
parents: 62754
diff changeset
    73
wenzelm
parents: 62754
diff changeset
    74
  def session_list(): List[String] =
wenzelm
parents: 62754
diff changeset
    75
  {
wenzelm
parents: 62754
diff changeset
    76
    val session_tree = Sessions.load(PIDE.options.value, dirs = session_dirs())
wenzelm
parents: 62754
diff changeset
    77
    val (main_sessions, other_sessions) =
wenzelm
parents: 62754
diff changeset
    78
      session_tree.topological_order.partition(p => p._2.groups.contains("main"))
wenzelm
parents: 62754
diff changeset
    79
    main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
wenzelm
parents: 62754
diff changeset
    80
  }
wenzelm
parents: 62754
diff changeset
    81
65210
8cfdf420b643 tuned signature;
wenzelm
parents: 64909
diff changeset
    82
  def session_base(): Sessions.Base =
62972
wenzelm
parents: 62754
diff changeset
    83
  {
64856
5e9bf964510a clarified modules;
wenzelm
parents: 64732
diff changeset
    84
    val base =
65251
4b0a43afc3fb clarified modules;
wenzelm
parents: 65226
diff changeset
    85
      try { Sessions.session_base(PIDE.options.value, session_name(), session_dirs()) }
65254
3075aa3b40bf clarified fall-back base, e.g. relevant for "isabelle jedit -l BAD";
wenzelm
parents: 65252
diff changeset
    86
      catch { case ERROR(_) => Sessions.pure_base(PIDE.options.value) }
65252
8b776d12f6c0 map values statically;
wenzelm
parents: 65251
diff changeset
    87
    base.copy(known_theories =
8b776d12f6c0 map values statically;
wenzelm
parents: 65251
diff changeset
    88
      for ((a, b) <- base.known_theories) yield (a, b.map(File.platform_path(_))))
62972
wenzelm
parents: 62754
diff changeset
    89
  }
wenzelm
parents: 62754
diff changeset
    90
wenzelm
parents: 62754
diff changeset
    91
wenzelm
parents: 62754
diff changeset
    92
  /* logic selector */
wenzelm
parents: 62754
diff changeset
    93
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    94
  private class Logic_Entry(val name: String, val description: String)
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    95
  {
57912
wenzelm
parents: 57612
diff changeset
    96
    override def toString: String = description
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    97
  }
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    98
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
    99
  def logic_selector(autosave: Boolean): Option_Component =
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   100
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56890
diff changeset
   101
    GUI_Thread.require {}
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   102
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   103
    val entries =
61288
9399860edb46 clarified modules;
wenzelm
parents: 60992
diff changeset
   104
      new Logic_Entry("", "default (" + session_name() + ")") ::
62974
wenzelm
parents: 62973
diff changeset
   105
        session_list().map(name => new Logic_Entry(name, name))
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   106
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   107
    val component = new ComboBox(entries) with Option_Component {
50375
c101127a7f37 clarified logic argument: session name, not path name;
wenzelm
parents: 50205
diff changeset
   108
      name = option_name
49270
e5d162d15867 some support to organize options in sections;
wenzelm
parents: 49248
diff changeset
   109
      val title = "Logic"
49247
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   110
      def load: Unit =
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   111
      {
50375
c101127a7f37 clarified logic argument: session name, not path name;
wenzelm
parents: 50205
diff changeset
   112
        val logic = PIDE.options.string(option_name)
49247
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   113
        entries.find(_.name == logic) match {
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   114
          case Some(entry) => selection.item = entry
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   115
          case None =>
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   116
        }
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   117
      }
50375
c101127a7f37 clarified logic argument: session name, not path name;
wenzelm
parents: 50205
diff changeset
   118
      def save: Unit = PIDE.options.string(option_name) = selection.item.name
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   119
    }
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   120
49247
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   121
    component.load()
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   122
    if (autosave) {
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   123
      component.listenTo(component.selection)
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   124
      component.reactions += { case SelectionChanged(_) => component.save() }
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   125
    }
50380
b1cb76418760 select logic session names, not paths;
wenzelm
parents: 50375
diff changeset
   126
    component.tooltip = "Logic session name (change requires restart)"
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   127
    component
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   128
  }
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents:
diff changeset
   129
}