src/Tools/jEdit/src/isabelle_logic.scala
author wenzelm
Tue Mar 15 22:01:26 2016 +0100 (2016-03-15)
changeset 62631 c39614ddb80b
parent 62556 c115e69f457f
child 62633 e57416b649d5
permissions -rw-r--r--
clarified modules;
wenzelm@49246
     1
/*  Title:      Tools/jEdit/src/isabelle_logic.scala
wenzelm@49246
     2
    Author:     Makarius
wenzelm@49246
     3
wenzelm@61288
     4
Isabelle logic session.
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@49246
    16
object Isabelle_Logic
wenzelm@49246
    17
{
wenzelm@50403
    18
  private val option_name = "jedit_logic"
wenzelm@50403
    19
wenzelm@61288
    20
  def session_name(): String =
wenzelm@50403
    21
    Isabelle_System.default_logic(
wenzelm@50403
    22
      Isabelle_System.getenv("JEDIT_LOGIC"),
wenzelm@50403
    23
      PIDE.options.string(option_name))
wenzelm@49246
    24
wenzelm@49246
    25
  private class Logic_Entry(val name: String, val description: String)
wenzelm@49246
    26
  {
wenzelm@57912
    27
    override def toString: String = description
wenzelm@49246
    28
  }
wenzelm@49246
    29
wenzelm@49246
    30
  def logic_selector(autosave: Boolean): Option_Component =
wenzelm@49246
    31
  {
wenzelm@57612
    32
    GUI_Thread.require {}
wenzelm@49246
    33
wenzelm@49246
    34
    val entries =
wenzelm@61288
    35
      new Logic_Entry("", "default (" + session_name() + ")") ::
wenzelm@50380
    36
        Isabelle_Logic.session_list().map(name => new Logic_Entry(name, name))
wenzelm@49246
    37
wenzelm@49246
    38
    val component = new ComboBox(entries) with Option_Component {
wenzelm@50375
    39
      name = option_name
wenzelm@49270
    40
      val title = "Logic"
wenzelm@49247
    41
      def load: Unit =
wenzelm@49247
    42
      {
wenzelm@50375
    43
        val logic = PIDE.options.string(option_name)
wenzelm@49247
    44
        entries.find(_.name == logic) match {
wenzelm@49247
    45
          case Some(entry) => selection.item = entry
wenzelm@49247
    46
          case None =>
wenzelm@49247
    47
        }
wenzelm@49247
    48
      }
wenzelm@50375
    49
      def save: Unit = PIDE.options.string(option_name) = selection.item.name
wenzelm@49246
    50
    }
wenzelm@49246
    51
wenzelm@49247
    52
    component.load()
wenzelm@49246
    53
    if (autosave) {
wenzelm@49246
    54
      component.listenTo(component.selection)
wenzelm@49246
    55
      component.reactions += { case SelectionChanged(_) => component.save() }
wenzelm@49246
    56
    }
wenzelm@50380
    57
    component.tooltip = "Logic session name (change requires restart)"
wenzelm@49246
    58
    component
wenzelm@49246
    59
  }
wenzelm@49246
    60
wenzelm@61288
    61
  def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
wenzelm@61288
    62
wenzelm@61288
    63
  def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
wenzelm@49246
    64
  {
wenzelm@61288
    65
    val mode = session_build_mode()
wenzelm@61288
    66
wenzelm@61288
    67
    Build.build(options = PIDE.options.value, progress = progress,
wenzelm@61288
    68
      build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
wenzelm@61288
    69
      dirs = session_dirs(), sessions = List(session_name()))
wenzelm@61288
    70
  }
wenzelm@61288
    71
wenzelm@62556
    72
  def session_start()
wenzelm@61288
    73
  {
wenzelm@62556
    74
    val modes =
wenzelm@62556
    75
      (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
wenzelm@62556
    76
       space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
wenzelm@62556
    77
    PIDE.session.start(receiver =>
wenzelm@62556
    78
      Isabelle_Process(
wenzelm@62556
    79
        PIDE.options.value, heap = session_name(), modes = modes, receiver = receiver))
wenzelm@49246
    80
  }
wenzelm@49246
    81
wenzelm@50380
    82
  def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
wenzelm@50380
    83
wenzelm@50380
    84
  def session_list(): List[String] =
wenzelm@50380
    85
  {
wenzelm@62631
    86
    val session_tree = Sessions.find(PIDE.options.value, dirs = session_dirs())
wenzelm@50574
    87
    val (main_sessions, other_sessions) =
wenzelm@50574
    88
      session_tree.topological_order.partition(p => p._2.groups.contains("main"))
wenzelm@50574
    89
    main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
wenzelm@50380
    90
  }
wenzelm@50380
    91
wenzelm@49246
    92
  def session_content(inlined_files: Boolean): Build.Session_Content =
wenzelm@49246
    93
  {
wenzelm@61288
    94
    val content =
wenzelm@61288
    95
      Build.session_content(PIDE.options.value, inlined_files, session_dirs(), session_name())
wenzelm@56801
    96
    content.copy(known_theories =
wenzelm@60992
    97
      content.known_theories.mapValues(name => name.map(File.platform_path(_))))
wenzelm@49246
    98
  }
wenzelm@49246
    99
}