src/Tools/jEdit/src/jedit_sessions.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64732 00f3c4bef2e0
child 64856 5e9bf964510a
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@62973
     4
Isabelle/jEdit session information.
wenzelm@49246
     5
*/
wenzelm@49246
     6
wenzelm@49246
     7
package isabelle.jedit
wenzelm@49246
     8
wenzelm@49246
     9
wenzelm@49246
    10
import isabelle._
wenzelm@49246
    11
wenzelm@49246
    12
import scala.swing.ComboBox
wenzelm@49246
    13
import scala.swing.event.SelectionChanged
wenzelm@49246
    14
wenzelm@49246
    15
wenzelm@62973
    16
object JEdit_Sessions
wenzelm@49246
    17
{
wenzelm@62972
    18
  /* session info */
wenzelm@62972
    19
wenzelm@50403
    20
  private val option_name = "jedit_logic"
wenzelm@50403
    21
wenzelm@64602
    22
  sealed case class Info(name: String, open_root: Position.T)
wenzelm@49246
    23
wenzelm@62972
    24
  def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
wenzelm@62972
    25
wenzelm@63986
    26
  def session_options(): Options =
wenzelm@63986
    27
    Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
wenzelm@63986
    28
      case "" => PIDE.options.value
wenzelm@63986
    29
      case s => PIDE.options.value.string("ML_process_policy") = s
wenzelm@63986
    30
    }
wenzelm@63986
    31
wenzelm@64602
    32
  def session_info(): Info =
wenzelm@64602
    33
  {
wenzelm@64602
    34
    val logic =
wenzelm@64602
    35
      Isabelle_System.default_logic(
wenzelm@64602
    36
        Isabelle_System.getenv("JEDIT_LOGIC"),
wenzelm@64602
    37
        PIDE.options.string(option_name))
wenzelm@64602
    38
wenzelm@64602
    39
    (for {
wenzelm@64602
    40
      tree <-
wenzelm@64602
    41
        try { Some(Sessions.load(session_options(), dirs = session_dirs())) }
wenzelm@64602
    42
        catch { case ERROR(_) => None }
wenzelm@64602
    43
      info <- tree.lift(logic)
wenzelm@64602
    44
      parent <- info.parent
wenzelm@64602
    45
      if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
wenzelm@64602
    46
    } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
wenzelm@64602
    47
  }
wenzelm@64602
    48
wenzelm@64602
    49
  def session_name(): String = session_info().name
wenzelm@64602
    50
wenzelm@62972
    51
  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
wenzelm@62972
    52
wenzelm@62972
    53
  def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
wenzelm@62972
    54
  {
wenzelm@62972
    55
    val mode = session_build_mode()
wenzelm@62972
    56
wenzelm@63986
    57
    Build.build(options = session_options(), progress = progress,
wenzelm@62972
    58
      build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
wenzelm@62972
    59
      dirs = session_dirs(), sessions = List(session_name())).rc
wenzelm@62972
    60
  }
wenzelm@62972
    61
wenzelm@62972
    62
  def session_start()
wenzelm@62972
    63
  {
wenzelm@62972
    64
    val modes =
wenzelm@62972
    65
      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
wenzelm@62972
    66
       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
wenzelm@63986
    67
wenzelm@62972
    68
    PIDE.session.start(receiver =>
wenzelm@63986
    69
      Isabelle_Process(options = session_options(), logic = session_name(), dirs = session_dirs(),
wenzelm@62972
    70
        modes = modes, receiver = receiver,
wenzelm@62972
    71
        store = Sessions.store(session_build_mode() == "system")))
wenzelm@62972
    72
  }
wenzelm@62972
    73
wenzelm@62972
    74
  def session_list(): List[String] =
wenzelm@62972
    75
  {
wenzelm@62972
    76
    val session_tree = Sessions.load(PIDE.options.value, dirs = session_dirs())
wenzelm@62972
    77
    val (main_sessions, other_sessions) =
wenzelm@62972
    78
      session_tree.topological_order.partition(p => p._2.groups.contains("main"))
wenzelm@62972
    79
    main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
wenzelm@62972
    80
  }
wenzelm@62972
    81
wenzelm@62972
    82
  def session_content(inlined_files: Boolean): Build.Session_Content =
wenzelm@62972
    83
  {
wenzelm@62972
    84
    val content =
wenzelm@64602
    85
      try {
wenzelm@64602
    86
        Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
wenzelm@64602
    87
      }
wenzelm@64732
    88
      catch { case ERROR(_) => Build.Session_Content.empty }
wenzelm@62972
    89
    content.copy(known_theories =
wenzelm@62972
    90
      content.known_theories.mapValues(name => name.map(File.platform_path(_))))
wenzelm@62972
    91
  }
wenzelm@62972
    92
wenzelm@62972
    93
wenzelm@62972
    94
  /* logic selector */
wenzelm@62972
    95
wenzelm@49246
    96
  private class Logic_Entry(val name: String, val description: String)
wenzelm@49246
    97
  {
wenzelm@57912
    98
    override def toString: String = description
wenzelm@49246
    99
  }
wenzelm@49246
   100
wenzelm@49246
   101
  def logic_selector(autosave: Boolean): Option_Component =
wenzelm@49246
   102
  {
wenzelm@57612
   103
    GUI_Thread.require {}
wenzelm@49246
   104
wenzelm@49246
   105
    val entries =
wenzelm@61288
   106
      new Logic_Entry("", "default (" + session_name() + ")") ::
wenzelm@62974
   107
        session_list().map(name => new Logic_Entry(name, name))
wenzelm@49246
   108
wenzelm@49246
   109
    val component = new ComboBox(entries) with Option_Component {
wenzelm@50375
   110
      name = option_name
wenzelm@49270
   111
      val title = "Logic"
wenzelm@49247
   112
      def load: Unit =
wenzelm@49247
   113
      {
wenzelm@50375
   114
        val logic = PIDE.options.string(option_name)
wenzelm@49247
   115
        entries.find(_.name == logic) match {
wenzelm@49247
   116
          case Some(entry) => selection.item = entry
wenzelm@49247
   117
          case None =>
wenzelm@49247
   118
        }
wenzelm@49247
   119
      }
wenzelm@50375
   120
      def save: Unit = PIDE.options.string(option_name) = selection.item.name
wenzelm@49246
   121
    }
wenzelm@49246
   122
wenzelm@49247
   123
    component.load()
wenzelm@49246
   124
    if (autosave) {
wenzelm@49246
   125
      component.listenTo(component.selection)
wenzelm@49246
   126
      component.reactions += { case SelectionChanged(_) => component.save() }
wenzelm@49246
   127
    }
wenzelm@50380
   128
    component.tooltip = "Logic session name (change requires restart)"
wenzelm@49246
   129
    component
wenzelm@49246
   130
  }
wenzelm@49246
   131
}