diff --git a/src/Tools/jEdit/src/jedit_sessions.scala b/src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala +++ b/src/Tools/jEdit/src/jedit_sessions.scala @@ -1,150 +1,150 @@ /* Title: Tools/jEdit/src/jedit_sessions.scala Author: Makarius Isabelle/jEdit session information, based on implicit process environment and explicit options. */ package isabelle.jedit import isabelle._ import scala.swing.ComboBox import scala.swing.event.SelectionChanged object JEdit_Sessions { /* session options */ def session_dirs: List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-") def session_no_build: Boolean = Isabelle_System.getenv("JEDIT_NO_BUILD") == "true" def session_options(options: Options): Options = { val options1 = Isabelle_System.getenv("JEDIT_BUILD_MODE") match { case "default" => options case mode => options.bool.update("system_heaps", mode == "system") } val options2 = Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match { case "" => options1 case s => options1.string.update("ML_process_policy", s) } options2 } def sessions_structure( options: Options = PIDE.options.value, dirs: List[Path] = session_dirs ): Sessions.Structure = { Sessions.load_structure(session_options(options), dirs = dirs) } /* raw logic info */ private val jedit_logic_option = "jedit_logic" def logic_name(options: Options): String = Isabelle_System.default_logic( Isabelle_System.getenv("JEDIT_LOGIC"), options.string(jedit_logic_option)) def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR")) def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true" def logic_include_sessions: List[String] = space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS")) def logic_info(options: Options): Option[Sessions.Info] = try { sessions_structure(options = options).get(logic_name(options)) } catch { case ERROR(_) => None } def logic_root(options: Options): Position.T = if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none else Position.none /* logic selector */ private sealed case class Logic_Entry(name: String = "", description: String = "") { override def toString: String = proper_string(description) getOrElse name } def logic_selector(options: Options_Variable, autosave: Boolean = false): Option_Component = { GUI_Thread.require {} val default_entry = Logic_Entry(description = "default (" + logic_name(options.value) + ")") val session_entries = { val sessions = sessions_structure(options = options.value) val (main_sessions, other_sessions) = sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main")) (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name)) } val entries = default_entry :: session_entries - new ComboBox(entries) with Option_Component { + new ComboBox[Logic_Entry](entries) with Option_Component { name = jedit_logic_option tooltip = "Logic session name (change requires restart)" val title = "Logic" def load(): Unit = { val logic = options.string(jedit_logic_option) entries.find(_.name == logic) match { case Some(entry) => selection.item = entry case None => } } def save(): Unit = options.string(jedit_logic_option) = selection.item.name load() if (autosave) { listenTo(selection) reactions += { case SelectionChanged(_) => save() } } } } /* session build process */ def session_base_info(options: Options): Sessions.Base_Info = Sessions.base_info(options, dirs = JEdit_Sessions.session_dirs, include_sessions = logic_include_sessions, session = logic_name(options), session_ancestor = logic_ancestor, session_requirements = logic_requirements) def session_build( options: Options, progress: Progress = new Progress, no_build: Boolean = false ): Int = { Build.build(session_options(options), selection = Sessions.Selection.session(PIDE.resources.session_base.session_name), progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs, infos = PIDE.resources.session_base_info.infos).rc } def session_start(options0: Options): Unit = { val session = PIDE.session val options = session_options(options0) val sessions_structure = PIDE.resources.session_base_info.sessions_structure val store = Sessions.store(options) session.phase_changed += PIDE.plugin.session_phase_changed Isabelle_Process.start(session, options, sessions_structure, store, logic = PIDE.resources.session_base.session_name, modes = (space_explode(',', options.string("jedit_print_mode")) ::: space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse) } } diff --git a/src/Tools/jEdit/src/jedit_spell_checker.scala b/src/Tools/jEdit/src/jedit_spell_checker.scala --- a/src/Tools/jEdit/src/jedit_spell_checker.scala +++ b/src/Tools/jEdit/src/jedit_spell_checker.scala @@ -1,107 +1,107 @@ /* Title: Tools/jEdit/src/jedit_spell_checker.scala Author: Makarius Specific spell-checker support for Isabelle/jEdit. */ package isabelle.jedit import isabelle._ import javax.swing.JMenuItem import scala.swing.ComboBox import org.gjt.sp.jedit.menu.EnhancedMenuItem import org.gjt.sp.jedit.jEdit import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} object JEdit_Spell_Checker { /* completion */ def completion( rendering: JEdit_Rendering, explicit: Boolean, caret: Text.Offset ): Option[Completion.Result] = { PIDE.plugin.spell_checker.get match { case Some(spell_checker) if explicit => spell_checker.completion(rendering, caret) case _ => None } } /* context menu */ def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] = { val result = for { spell_checker <- PIDE.plugin.spell_checker.get doc_view <- Document_View.get(text_area) rendering = doc_view.get_rendering() range = JEdit_Lib.point_range(text_area.getBuffer, offset) Text.Info(_, word) <- Spell_Checker.current_word(rendering, range) } yield (spell_checker, word) result match { case Some((spell_checker, word)) => val context = jEdit.getActionContext() def item(name: String): JMenuItem = new EnhancedMenuItem(context.getAction(name).getLabel, name, context) val complete_items = if (spell_checker.complete(word).nonEmpty) List(item("isabelle.complete-word")) else Nil val update_items = if (spell_checker.check(word)) List(item("isabelle.exclude-word"), item("isabelle.exclude-word-permanently")) else List(item("isabelle.include-word"), item("isabelle.include-word-permanently")) val reset_items = spell_checker.reset_enabled() match { case 0 => Nil case n => val name = "isabelle.reset-words" val label = context.getAction(name).getLabel List(new EnhancedMenuItem(label + " (" + n + ")", name, context)) } complete_items ::: update_items ::: reset_items case None => Nil } } /* dictionaries */ def dictionaries_selector(): Option_Component = { GUI_Thread.require {} val option_name = "spell_checker_dictionary" val opt = PIDE.options.value.check_name(option_name) val entries = Spell_Checker.dictionaries - val component = new ComboBox(entries) with Option_Component { + + new ComboBox[Spell_Checker.Dictionary](entries) with Option_Component { name = option_name + tooltip = GUI.tooltip_lines(opt.print_default) val title = opt.title() def load(): Unit = { val lang = PIDE.options.string(option_name) entries.find(_.lang == lang) match { case Some(entry) => selection.item = entry case None => } } def save(): Unit = PIDE.options.string(option_name) = selection.item.lang - } - component.load() - component.tooltip = GUI.tooltip_lines(opt.print_default) - component + load() + } } }