src/Tools/jEdit/src/jedit_sessions.scala
changeset 63986 c7a4b03727ae
parent 62974 f17602cbf76a
child 64602 8edca3465758
equal deleted inserted replaced
63985:4effb93c2a09 63986:c7a4b03727ae
    24       Isabelle_System.getenv("JEDIT_LOGIC"),
    24       Isabelle_System.getenv("JEDIT_LOGIC"),
    25       PIDE.options.string(option_name))
    25       PIDE.options.string(option_name))
    26 
    26 
    27   def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    27   def session_dirs(): List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
    28 
    28 
       
    29   def session_options(): Options =
       
    30     Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
       
    31       case "" => PIDE.options.value
       
    32       case s => PIDE.options.value.string("ML_process_policy") = s
       
    33     }
       
    34 
    29   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    35   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")
    30 
    36 
    31   def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
    37   def session_build(progress: Progress = Ignore_Progress, no_build: Boolean = false): Int =
    32   {
    38   {
    33     val mode = session_build_mode()
    39     val mode = session_build_mode()
    34 
    40 
    35     Build.build(options = PIDE.options.value, progress = progress,
    41     Build.build(options = session_options(), progress = progress,
    36       build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
    42       build_heap = true, no_build = no_build, system_mode = mode == "" || mode == "system",
    37       dirs = session_dirs(), sessions = List(session_name())).rc
    43       dirs = session_dirs(), sessions = List(session_name())).rc
    38   }
    44   }
    39 
    45 
    40   def session_start()
    46   def session_start()
    41   {
    47   {
    42     val modes =
    48     val modes =
    43       (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
    49       (space_explode(',', PIDE.options.string("jedit_print_mode")) :::
    44        space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
    50        space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse
       
    51 
    45     PIDE.session.start(receiver =>
    52     PIDE.session.start(receiver =>
    46       Isabelle_Process(PIDE.options.value, logic = session_name(), dirs = session_dirs(),
    53       Isabelle_Process(options = session_options(), logic = session_name(), dirs = session_dirs(),
    47         modes = modes, receiver = receiver,
    54         modes = modes, receiver = receiver,
    48         store = Sessions.store(session_build_mode() == "system")))
    55         store = Sessions.store(session_build_mode() == "system")))
    49   }
    56   }
    50 
    57 
    51   def session_list(): List[String] =
    58   def session_list(): List[String] =