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