diff --git a/src/Pure/System/options.scala b/src/Pure/System/options.scala --- a/src/Pure/System/options.scala +++ b/src/Pure/System/options.scala @@ -1,478 +1,479 @@ /* Title: Pure/System/options.scala Author: Makarius System options with external string representation. */ package isabelle object Options { type Spec = (String, Option[String]) val empty: Options = new Options() /* typed access */ abstract class Access[A](val options: Options) { def apply(name: String): A def update(name: String, x: A): Options def change(name: String, f: A => A): Options = update(name, f(apply(name))) } class Access_Variable[A]( val options: Options_Variable, val pure_access: Options => Access[A] ) { def apply(name: String): A = pure_access(options.value)(name) def update(name: String, x: A): Unit = options.change(options => pure_access(options).update(name, x)) def change(name: String, f: A => A): Unit = update(name, f(apply(name))) } /* representation */ sealed abstract class Type { def print: String = Word.lowercase(toString) } case object Bool extends Type case object Int extends Type case object Real extends Type case object String extends Type case object Unknown extends Type val TAG_CONTENT = "content" // formal theory content val TAG_DOCUMENT = "document" // document preparation val TAG_BUILD = "build" // relavant for "isabelle build" val TAG_UPDATE = "update" // relevant for "isabelle update" val TAG_CONNECTION = "connection" // private information about connections (password etc.) + val TAG_COLOR_DIALOG = "color_dialog" // special color selection dialog case class Entry( public: Boolean, pos: Position.T, name: String, typ: Type, value: String, default_value: String, standard_value: Option[String], tags: List[String], description: String, section: String ) { private def print_value(x: String): String = if (typ == Options.String) quote(x) else x private def print_standard: String = standard_value match { case None => "" case Some(s) if s == default_value => " (standard)" case Some(s) => " (standard " + print_value(s) + ")" } private def print(default: Boolean): String = { val x = if (default) default_value else value "option " + name + " : " + typ.print + " = " + print_value(x) + print_standard + if_proper(description, "\n -- " + quote(description)) } def print: String = print(false) def print_default: String = print(true) def title(strip: String = ""): String = { val words = Word.explode('_', name) val words1 = words match { case word :: rest if word == strip => rest case _ => words } Word.implode(words1.map(Word.perhaps_capitalize)) } def title_jedit: String = title("jedit") def unknown: Boolean = typ == Unknown def has_tag(tag: String): Boolean = tags.contains(tag) - def session_content: Boolean = has_tag(TAG_CONTENT) || has_tag(TAG_DOCUMENT) + def color_dialog: Boolean = has_tag(TAG_COLOR_DIALOG) } /* parsing */ private val SECTION = "section" private val PUBLIC = "public" private val OPTION = "option" private val STANDARD = "standard" private val FOR = "for" private val OPTIONS = Path.explode("etc/options") private val PREFS = Path.explode("$ISABELLE_HOME_USER/etc/preferences") val options_syntax: Outer_Syntax = Outer_Syntax.empty + ":" + "=" + "--" + "(" + ")" + Symbol.comment + Symbol.comment_decoded + (SECTION, Keyword.DOCUMENT_HEADING) + (PUBLIC, Keyword.BEFORE_COMMAND) + (OPTION, Keyword.THY_DECL) + STANDARD + FOR val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "=" trait Parsers extends Parse.Parsers { val option_name: Parser[String] = atom("option name", _.is_name) val option_type: Parser[String] = atom("option type", _.is_name) val option_value: Parser[String] = opt(token("-", tok => tok.is_sym_ident && tok.content == "-")) ~ atom("nat", _.is_nat) ^^ { case s ~ n => if (s.isDefined) "-" + n else n } | atom("option value", tok => tok.is_name || tok.is_float) val option_standard: Parser[Option[String]] = $$$("(") ~! $$$(STANDARD) ~ opt(option_value) ~ $$$(")") ^^ { case _ ~ _ ~ a ~ _ => a } val option_tag: Parser[String] = atom("option tag", _.is_name) val option_tags: Parser[List[String]] = $$$(FOR) ~! rep(option_tag) ^^ { case _ ~ x => x } | success(Nil) } private object Parsers extends Parsers { def comment_marker: Parser[String] = $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded) val option_entry: Parser[Options => Options] = { command(SECTION) ~! text ^^ { case _ ~ a => (options: Options) => options.set_section(a) } | opt($$$(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~ $$$("=") ~ option_value ~ opt(option_standard) ~ option_tags ~ (comment_marker ~! text ^^ { case _ ~ x => x } | success(""))) ^^ { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e ~ f ~ g) => (options: Options) => options.declare(a.isDefined, pos, b, c, d, e, f, g) } } val prefs_entry: Parser[Options => Options] = { option_name ~ ($$$("=") ~! option_value) ^^ { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) } } def parse_file( options: Options, file_name: String, content: String, syntax: Outer_Syntax = options_syntax, parser: Parser[Options => Options] = option_entry ): Options = { val toks = Token.explode(syntax.keywords, content) val ops = parse_all(rep(parser), Token.reader(toks, Token.Pos.file(file_name))) match { case Success(result, _) => result case bad => error(bad.toString) } try { ops.foldLeft(options.set_section("")) { case (opts, op) => op(opts) } } catch { case ERROR(msg) => error(msg + Position.here(Position.File(file_name))) } } def parse_prefs(options: Options, content: String): Options = parse_file(options, PREFS.file_name, content, syntax = prefs_syntax, parser = prefs_entry) } def read_prefs(file: Path = PREFS): String = if (file.is_file) File.read(file) else "" def init(prefs: String = read_prefs(PREFS), opts: List[String] = Nil): Options = { var options = empty for { dir <- Components.directories() file = dir + OPTIONS if file.is_file } { options = Parsers.parse_file(options, file.implode, File.read(file)) } opts.foldLeft(Parsers.parse_prefs(options, prefs))(_ + _) } def init0(): Options = init(prefs = "") /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("options", "print Isabelle system options", Scala_Project.here, { args => var build_options = false var get_option = "" var list_options = false var export_file = "" val getopts = Getopts(""" Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] Options are: -b include $ISABELLE_BUILD_OPTIONS -g OPTION get value of OPTION -l list options -x FILE export options to FILE in YXML format Report Isabelle system options, augmented by MORE_OPTIONS given as arguments NAME=VAL or NAME. """, "b" -> (_ => build_options = true), "g:" -> (arg => get_option = arg), "l" -> (_ => list_options = true), "x:" -> (arg => export_file = arg)) val more_options = getopts(args) if (get_option == "" && !list_options && export_file == "") getopts.usage() val options = { val options0 = Options.init() val options1 = if (build_options) Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _) else options0 more_options.foldLeft(options1)(_ + _) } if (get_option != "") Output.writeln(options.check_name(get_option).value, stdout = true) if (export_file != "") File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) if (get_option == "" && export_file == "") Output.writeln(options.print, stdout = true) }) } final class Options private( options: Map[String, Options.Entry] = Map.empty, val section: String = "" ) { def iterator: Iterator[Options.Entry] = options.valuesIterator override def toString: String = iterator.mkString("Options(", ",", ")") private def print_entry(opt: Options.Entry): String = if (opt.public) "public " + opt.print else opt.print def print: String = cat_lines(iterator.toList.sortBy(_.name).map(print_entry)) def description(name: String): String = check_name(name).description /* check */ def get(name: String): Option[Options.Entry] = options.get(name) def check_name(name: String): Options.Entry = get(name) match { case Some(opt) if !opt.unknown => opt case _ => error("Unknown option " + quote(name)) } private def check_type(name: String, typ: Options.Type): Options.Entry = { val opt = check_name(name) if (opt.typ == typ) opt else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print) } /* basic operations */ private def put(name: String, typ: Options.Type, value: String): Options = { val opt = check_type(name, typ) new Options(options + (name -> opt.copy(value = value)), section) } private def get[A](name: String, typ: Options.Type, parse: String => Option[A]): A = { val opt = check_type(name, typ) parse(opt.value) match { case Some(x) => x case None => error("Malformed value for option " + quote(name) + " : " + typ.print + " =\n" + quote(opt.value)) } } /* internal lookup and update */ val bool: Options.Access[Boolean] = new Options.Access[Boolean](this) { def apply(name: String): Boolean = get(name, Options.Bool, Value.Boolean.unapply) def update(name: String, x: Boolean): Options = put(name, Options.Bool, Value.Boolean(x)) } val int: Options.Access[Int] = new Options.Access[Int](this) { def apply(name: String): Int = get(name, Options.Int, Value.Int.unapply) def update(name: String, x: Int): Options = put(name, Options.Int, Value.Int(x)) } val real: Options.Access[Double] = new Options.Access[Double](this) { def apply(name: String): Double = get(name, Options.Real, Value.Double.unapply) def update(name: String, x: Double): Options = put(name, Options.Real, Value.Double(x)) } val string: Options.Access[String] = new Options.Access[String](this) { def apply(name: String): String = get(name, Options.String, Some(_)) def update(name: String, x: String): Options = put(name, Options.String, x) } def proper_string(name: String): Option[String] = Library.proper_string(string(name)) def seconds(name: String): Time = Time.seconds(real(name)) /* external updates */ private def check_value(name: String): Options = { val opt = check_name(name) opt.typ match { case Options.Bool => bool(name); this case Options.Int => int(name); this case Options.Real => real(name); this case Options.String => string(name); this case Options.Unknown => this } } def declare( public: Boolean, pos: Position.T, name: String, typ_name: String, value: String, standard: Option[Option[String]], tags: List[String], description: String ): Options = { get(name) match { case Some(other) => error("Duplicate declaration of option " + quote(name) + Position.here(pos) + Position.here(other.pos)) case None => val typ = typ_name match { case "bool" => Options.Bool case "int" => Options.Int case "real" => Options.Real case "string" => Options.String case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name) + Position.here(pos)) } val standard_value = standard match { case None => None case Some(_) if typ == Options.Bool => error("Illegal standard value for option " + quote(name) + " : " + typ_name + Position.here) case Some(s) => Some(s.getOrElse(value)) } val opt = Options.Entry( public, pos, name, typ, value, value, standard_value, tags, description, section) (new Options(options + (name -> opt), section)).check_value(name) } } def add_permissive(name: String, value: String): Options = { if (options.isDefinedAt(name)) this + (name, value) else { val opt = Options.Entry(false, Position.none, name, Options.Unknown, value, value, None, Nil, "", "") new Options(options + (name -> opt), section) } } def + (name: String, value: String): Options = { val opt = check_name(name) (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name) } def + (name: String, opt_value: Option[String]): Options = { val opt = check_name(name) opt_value orElse opt.standard_value match { case Some(value) => this + (name, value) case None if opt.typ == Options.Bool => this + (name, "true") case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print) } } def + (str: String): Options = str match { case Properties.Eq(a, b) => this + (a, b) case _ => this + (str, None) } def ++ (specs: List[Options.Spec]): Options = specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) } /* sections */ def set_section(new_section: String): Options = new Options(options, new_section) def sections: List[(String, List[Options.Entry])] = options.groupBy(_._2.section).toList.map({ case (a, opts) => (a, opts.toList.map(_._2)) }) /* encode */ def encode: XML.Body = { val opts = for ((_, opt) <- options.toList; if !opt.unknown) yield (opt.pos, (opt.name, (opt.typ.print, opt.value))) import XML.Encode.{string => string_, _} list(pair(properties, pair(string_, pair(string_, string_))))(opts) } /* preferences */ def make_prefs( defaults: Options = Options.init0(), filter: Options.Entry => Boolean = _ => true ): String = { (for { (name, opt2) <- options.iterator opt1 = defaults.get(name) if (opt1.isEmpty || opt1.get.value != opt2.value) && filter(opt2) } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else "")) .toList.sortBy(_._1) .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString } def session_prefs(defaults: Options = Options.init0()): String = make_prefs(defaults = defaults, filter = _.session_content) def save_prefs(file: Path = Options.PREFS, defaults: Options = Options.init0()): Unit = { val prefs = make_prefs(defaults = defaults) Isabelle_System.make_directory(file.dir) File.write_backup(file, "(* generated by Isabelle " + Date.now() + " *)\n\n" + prefs) } } class Options_Variable(init_options: Options) { private var _options = init_options def value: Options = synchronized { _options } def change(f: Options => Options): Unit = synchronized { _options = f(_options) } def += (name: String, x: String): Unit = change(options => options + (name, x)) val bool: Options.Access_Variable[Boolean] = new Options.Access_Variable[Boolean](this, _.bool) val int: Options.Access_Variable[Int] = new Options.Access_Variable[Int](this, _.int) val real: Options.Access_Variable[Double] = new Options.Access_Variable[Double](this, _.real) val string: Options.Access_Variable[String] = new Options.Access_Variable[String](this, _.string) def proper_string(name: String): Option[String] = Library.proper_string(string(name)) def seconds(name: String): Time = value.seconds(name) } diff --git a/src/Tools/jEdit/etc/options b/src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options +++ b/src/Tools/jEdit/etc/options @@ -1,169 +1,169 @@ (* :mode=isabelle-options: *) public option jedit_logic : string = "" -- "logic session name (change requires restart)" public option jedit_print_mode : string = "" -- "default print modes for output, separated by commas (change requires restart)" public option jedit_auto_resolve : bool = false -- "automatically resolve auxiliary files within the document model" public option jedit_reset_font_size : int = 18 -- "reset main text font size" public option jedit_font_scale : real = 1.0 -- "scale factor of add-on panels wrt. main text font" public option jedit_popup_font_scale : real = 0.85 -- "scale factor of popups wrt. main text font" public option jedit_popup_bounds : real = 0.5 -- "relative bounds of popup window wrt. logical screen size" public option jedit_tooltip_delay : real = 0.75 -- "open/close delay for document tooltips (seconds)" public option jedit_tooltip_margin : int = 60 -- "margin for tooltip pretty-printing" public option jedit_structure_limit : int = 1000 -- "maximum number of lines to scan for language structure" public option jedit_symbols_search_limit : int = 50 -- "maximum number of symbols in search result" public option jedit_timing_threshold : real = 0.1 -- "default threshold for timing display (seconds)" public option jedit_text_overview : bool = true -- "paint text overview column" public option jedit_focus_modifier : string = "CS" -- "keyboard modifier to enable entity focus regardless of def visibility" public option jedit_toggle_full_screen : bool = false -- "use original jEdit action toggle-full-screen instead of Isabelle/jEdit variant" public option isabelle_fonts_hinted : bool = true -- "use hinted Isabelle DejaVu fonts (change requires restart)" section "Indentation" public option jedit_indent_input : bool = true -- "indentation of Isabelle keywords after input (typed character or completion)" public option jedit_indent_newline : bool = true -- "indentation of Isabelle keywords on ENTER (action isabelle.newline)" public option jedit_indent_script : bool = true -- "indent unstructured proof script ('apply' etc.) via number of subgoals" public option jedit_indent_script_limit : int = 20 -- "maximum indentation of unstructured proof script ('apply' etc.)" section "Completion" public option jedit_completion : bool = true -- "enable completion popup" public option jedit_completion_select_enter : bool = false -- "select completion item via ENTER" public option jedit_completion_select_tab : bool = true -- "select completion item via TAB" public option jedit_completion_context : bool = true -- "use semantic language context for completion" public option jedit_completion_delay : real = 0.5 -- "delay for completion popup (seconds)" public option jedit_completion_immediate : bool = true -- "insert uniquely completed abbreviation immediately into buffer" section "Rendering of Document Content" -option outdated_color : string = "EEE3E3FF" -option unprocessed_color : string = "FFA0A0FF" -option unprocessed1_color : string = "FFA0A032" -option running_color : string = "610061FF" -option running1_color : string = "61006164" -option bullet_color : string = "000000FF" -option tooltip_color : string = "FFFFE9FF" -option writeln_color : string = "C0C0C0FF" -option information_color : string = "C1DFEEFF" -option warning_color : string = "FF8C00FF" -option legacy_color : string = "FF8C00FF" -option error_color : string = "B22222FF" -option ok_color : string = "000000FF" -option failed_color : string = "B22222FF" -option writeln_message_color : string = "F0F0F0FF" -option information_message_color : string = "DCEAF3FF" -option tracing_message_color : string = "F0F8FFFF" -option warning_message_color : string = "EEE8AAFF" -option legacy_message_color : string = "EEE8AAFF" -option error_message_color : string = "FFC1C1FF" -option spell_checker_color : string = "0000FFFF" -option bad_color : string = "FF6A6A64" -option canceled_color : string = "FF6A6A64" -option intensify_color : string = "FFCC6664" -option entity_color : string = "CCD9FF80" -option entity_ref_color : string = "800080FF" -option breakpoint_disabled_color : string = "CCCC0080" -option breakpoint_enabled_color : string = "FF9966FF" -option quoted_color : string = "8B8B8B19" -option antiquoted_color : string = "FFC83219" -option antiquote_color : string = "6600CCFF" -option raw_text_color : string = "6600CCFF" -option plain_text_color : string = "CC6600FF" -option highlight_color : string = "50505032" -option hyperlink_color : string = "000000FF" -option active_color : string = "DCDCDCFF" -option active_hover_color : string = "9DC75DFF" -option active_result_color : string = "999966FF" -option keyword1_color : string = "006699FF" -option keyword2_color : string = "009966FF" -option keyword3_color : string = "0099FFFF" -option quasi_keyword_color : string = "9966FFFF" -option improper_color : string = "FF5050FF" -option operator_color : string = "323232FF" -option comment1_color : string = "CC0000FF" -option comment2_color : string = "FF8400FF" -option comment3_color : string = "6600CCFF" -option caret_debugger_color : string = "FF9966FF" -option caret_invisible_color : string = "50000080" -option completion_color : string = "0000FFFF" -option search_color : string = "66FFFF64" +option outdated_color : string = "EEE3E3FF" for color_dialog +option unprocessed_color : string = "FFA0A0FF" for color_dialog +option unprocessed1_color : string = "FFA0A032" for color_dialog +option running_color : string = "610061FF" for color_dialog +option running1_color : string = "61006164" for color_dialog +option bullet_color : string = "000000FF" for color_dialog +option tooltip_color : string = "FFFFE9FF" for color_dialog +option writeln_color : string = "C0C0C0FF" for color_dialog +option information_color : string = "C1DFEEFF" for color_dialog +option warning_color : string = "FF8C00FF" for color_dialog +option legacy_color : string = "FF8C00FF" for color_dialog +option error_color : string = "B22222FF" for color_dialog +option ok_color : string = "000000FF" for color_dialog +option failed_color : string = "B22222FF" for color_dialog +option writeln_message_color : string = "F0F0F0FF" for color_dialog +option information_message_color : string = "DCEAF3FF" for color_dialog +option tracing_message_color : string = "F0F8FFFF" for color_dialog +option warning_message_color : string = "EEE8AAFF" for color_dialog +option legacy_message_color : string = "EEE8AAFF" for color_dialog +option error_message_color : string = "FFC1C1FF" for color_dialog +option spell_checker_color : string = "0000FFFF" for color_dialog +option bad_color : string = "FF6A6A64" for color_dialog +option canceled_color : string = "FF6A6A64" for color_dialog +option intensify_color : string = "FFCC6664" for color_dialog +option entity_color : string = "CCD9FF80" for color_dialog +option entity_ref_color : string = "800080FF" for color_dialog +option breakpoint_disabled_color : string = "CCCC0080" for color_dialog +option breakpoint_enabled_color : string = "FF9966FF" for color_dialog +option quoted_color : string = "8B8B8B19" for color_dialog +option antiquoted_color : string = "FFC83219" for color_dialog +option antiquote_color : string = "6600CCFF" for color_dialog +option raw_text_color : string = "6600CCFF" for color_dialog +option plain_text_color : string = "CC6600FF" for color_dialog +option highlight_color : string = "50505032" for color_dialog +option hyperlink_color : string = "000000FF" for color_dialog +option active_color : string = "DCDCDCFF" for color_dialog +option active_hover_color : string = "9DC75DFF" for color_dialog +option active_result_color : string = "999966FF" for color_dialog +option keyword1_color : string = "006699FF" for color_dialog +option keyword2_color : string = "009966FF" for color_dialog +option keyword3_color : string = "0099FFFF" for color_dialog +option quasi_keyword_color : string = "9966FFFF" for color_dialog +option improper_color : string = "FF5050FF" for color_dialog +option operator_color : string = "323232FF" for color_dialog +option comment1_color : string = "CC0000FF" for color_dialog +option comment2_color : string = "FF8400FF" for color_dialog +option comment3_color : string = "6600CCFF" for color_dialog +option caret_debugger_color : string = "FF9966FF" for color_dialog +option caret_invisible_color : string = "50000080" for color_dialog +option completion_color : string = "0000FFFF" for color_dialog +option search_color : string = "66FFFF64" for color_dialog -option tfree_color : string = "A020F0FF" -option tvar_color : string = "A020F0FF" -option free_color : string = "0000FFFF" -option skolem_color : string = "D2691EFF" -option bound_color : string = "008000FF" -option var_color : string = "00009BFF" -option inner_numeral_color : string = "FF0000FF" -option inner_quoted_color : string = "FF00CCFF" -option inner_cartouche_color : string = "CC6600FF" -option dynamic_color : string = "7BA428FF" -option class_parameter_color : string = "D2691EFF" +option tfree_color : string = "A020F0FF" for color_dialog +option tvar_color : string = "A020F0FF" for color_dialog +option free_color : string = "0000FFFF" for color_dialog +option skolem_color : string = "D2691EFF" for color_dialog +option bound_color : string = "008000FF" for color_dialog +option var_color : string = "00009BFF" for color_dialog +option inner_numeral_color : string = "FF0000FF" for color_dialog +option inner_quoted_color : string = "FF00CCFF" for color_dialog +option inner_cartouche_color : string = "CC6600FF" for color_dialog +option dynamic_color : string = "7BA428FF" for color_dialog +option class_parameter_color : string = "D2691EFF" for color_dialog -option markdown_bullet1_color : string = "DAFEDAFF" -option markdown_bullet2_color : string = "FFF0CCFF" -option markdown_bullet3_color : string = "E7E7FFFF" -option markdown_bullet4_color : string = "FFE0F0FF" +option markdown_bullet1_color : string = "DAFEDAFF" for color_dialog +option markdown_bullet2_color : string = "FFF0CCFF" for color_dialog +option markdown_bullet3_color : string = "E7E7FFFF" for color_dialog +option markdown_bullet4_color : string = "FFE0F0FF" for color_dialog section "Icons" option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png" option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png" option gutter_information_icon : string = "idea-icons/general/balloonInformation.png" option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png" option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png" option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png" option process_passive_icon : string = "idea-icons/process/step_passive.png" option process_active_icons : string = "idea-icons/process/step_1.png:idea-icons/process/step_2.png:idea-icons/process/step_3.png:idea-icons/process/step_4.png:idea-icons/process/step_5.png:idea-icons/process/step_6.png:idea-icons/process/step_7.png:idea-icons/process/step_8.png:idea-icons/process/step_9.png:idea-icons/process/step_10.png:idea-icons/process/step_11.png:idea-icons/process/step_12.png" diff --git a/src/Tools/jEdit/src/jedit_options.scala b/src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala +++ b/src/Tools/jEdit/src/jedit_options.scala @@ -1,214 +1,214 @@ /* Title: Tools/jEdit/src/jedit_options.scala Author: Makarius Options for Isabelle/jEdit. */ package isabelle.jedit import isabelle._ import java.awt.{Font, Color} import javax.swing.{InputVerifier, JComponent, UIManager} import javax.swing.text.JTextComponent import scala.swing.{Component, CheckBox, TextArea} import org.gjt.sp.jedit.gui.ColorWellButton import org.gjt.sp.jedit.{jEdit, AbstractOptionPane} object JEdit_Options { /* typed access and GUI components */ class Access[A](access: Options.Access_Variable[A], val name: String) { def description: String = access.options.value.description(name) def apply(): A = access.apply(name) def update(x: A): Unit = change(_ => x) def change(f: A => A): Unit = { val x0 = apply() access.change(name, f) val x1 = apply() if (x0 != x1) changed() } def changed(): Unit = GUI_Thread.require { PIDE.session.update_options(access.options.value) } } class Bool_Access(name: String) extends Access(PIDE.options.bool, name) { def set(): Unit = update(true) def reset(): Unit = update(false) def toggle(): Unit = change(b => !b) } class Bool_GUI(access: Bool_Access, label: String) extends GUI.Check(label, init = access()) { def load(): Unit = { selected = access() } override def clicked(state: Boolean): Unit = access.update(state) } /* specific options */ object continuous_checking extends Bool_Access("editor_continuous_checking") { override def changed(): Unit = { super.changed() PIDE.plugin.deps_changed() } class GUI extends Bool_GUI(this, "Continuous checking") { tooltip = "Continuous checking of proof document (visible and required parts)" } } object output_state extends Bool_Access("editor_output_state") { override def changed(): Unit = GUI_Thread.require { super.changed() PIDE.editor.flush_edits(hidden = true) PIDE.editor.flush() } class GUI extends Bool_GUI(this, "Proof state") { tooltip = "Output of proof state (normally shown on State panel)" } } /* editor pane for plugin options */ trait Entry extends Component { val title: String def load(): Unit def save(): Unit } abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) { protected val components: List[(String, List[Entry])] override def _init(): Unit = { val dummy_property = "options.isabelle.dummy" for ((s, cs) <- components) { if (s.nonEmpty) { jEdit.setProperty(dummy_property, s) addSeparator(dummy_property) jEdit.setProperty(dummy_property, null) } for (c <- cs) addComponent(c.title, c.peer) } } override def _save(): Unit = { for ((_, cs) <- components; c <- cs) c.save() } } class Isabelle_General_Options extends Isabelle_Options("isabelle-general") { val options: JEdit_Options = PIDE.options private val predefined = List( JEdit_Sessions.logic_selector(options), JEdit_Sessions.document_selector(options), JEdit_Spell_Checker.dictionaries_selector()) protected val components: List[(String, List[Entry])] = options.make_components(predefined, (for (opt <- options.value.iterator if opt.public) yield opt.name).toSet) } class Isabelle_Rendering_Options extends Isabelle_Options("isabelle-rendering") { private val predefined = (for { opt <- PIDE.options.value.iterator - if opt.name.endsWith("_color") && opt.section == "Rendering of Document Content" + if opt.color_dialog } yield PIDE.options.make_color_component(opt)).toList assert(predefined.nonEmpty) protected val components: List[(String, List[Entry])] = PIDE.options.make_components(predefined, _ => false) } } class JEdit_Options(init_options: Options) extends Options_Variable(init_options) { def color_value(s: String): Color = Color_Value(string(s)) def make_color_component(opt: Options.Entry): JEdit_Options.Entry = { GUI_Thread.require {} val opt_name = opt.name val opt_title = opt.title_jedit val button = new ColorWellButton(Color_Value(opt.value)) val component = new Component with JEdit_Options.Entry { override lazy val peer: JComponent = button name = opt_name val title: String = opt_title def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name))) def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor) } component.tooltip = GUI.tooltip_lines(opt.print_default) component } def make_component(opt: Options.Entry): JEdit_Options.Entry = { GUI_Thread.require {} val opt_name = opt.name val opt_title = opt.title_jedit val component = if (opt.typ == Options.Bool) new CheckBox with JEdit_Options.Entry { name = opt_name val title: String = opt_title def load(): Unit = selected = bool(opt_name) def save(): Unit = bool(opt_name) = selected } else { val default_font = GUI.copy_font(UIManager.getFont("TextField.font")) val text_area = new TextArea with JEdit_Options.Entry { if (default_font != null) font = default_font name = opt_name val title: String = opt_title def load(): Unit = text = value.check_name(opt_name).value def save(): Unit = try { JEdit_Options.this += (opt_name, text) } catch { case ERROR(msg) => GUI.error_dialog(this.peer, "Failed to update options", GUI.scrollable_text(msg)) } } text_area.peer.setInputVerifier({ case text: JTextComponent => try { value + (opt_name, text.getText); true } catch { case ERROR(_) => false } case _ => true }) GUI.plain_focus_traversal(text_area.peer) text_area } component.load() component.tooltip = GUI.tooltip_lines(opt.print_default) component } def make_components( predefined: List[JEdit_Options.Entry], filter: String => Boolean ) : List[(String, List[JEdit_Options.Entry])] = { def mk_component(opt: Options.Entry): List[JEdit_Options.Entry] = predefined.find(opt.name == _.name) match { case Some(c) => List(c) case None => if (filter(opt.name)) List(make_component(opt)) else Nil } value.sections.sortBy(_._1).map( { case (a, opts) => (a, opts.sortBy(_.title_jedit).flatMap(mk_component)) }) .filterNot(_._2.isEmpty) } }