--- a/NEWS Tue Sep 11 09:40:05 2012 +0200
+++ b/NEWS Tue Sep 11 11:53:34 2012 +0200
@@ -9,6 +9,12 @@
* Command 'ML_file' evaluates ML text from a file directly within the
theory, without any predeclaration via 'uses' in the theory header.
+* Old command 'use' command and corresponding keyword 'uses' in the
+theory header are legacy features and will be discontinued soon.
+Tools that load their additional source files may imitate the
+'ML_file' implementation, such that the system can take care of
+dependencies properly.
+
* Discontinued obsolete method fastsimp / tactic fast_simp_tac, which
is called fastforce / fast_force_tac already since Isabelle2011-1.
--- a/src/Doc/IsarRef/Spec.thy Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Doc/IsarRef/Spec.thy Tue Sep 11 11:53:34 2012 +0200
@@ -51,13 +51,11 @@
admissible.
@{rail "
- @@{command theory} @{syntax name} imports \\ keywords? uses? @'begin'
+ @@{command theory} @{syntax name} imports keywords? \\ @'begin'
;
imports: @'imports' (@{syntax name} +)
;
keywords: @'keywords' ((@{syntax string} +) ('::' @{syntax name} @{syntax tags})? + @'and')
- ;
- uses: @'uses' ((@{syntax name} | @{syntax parname}) +)
"}
\begin{description}
@@ -84,14 +82,6 @@
with and without proof, respectively. Additional @{syntax tags}
provide defaults for document preparation (\secref{sec:tags}).
- The optional @{keyword_def "uses"} specification declares additional
- dependencies on external files (notably ML sources). Files will be
- loaded immediately (as ML), unless the name is parenthesized. The
- latter case records a dependency that needs to be resolved later in
- the text, usually via explicit @{command_ref "use"} for ML files;
- other file formats require specific load commands defined by the
- corresponding tools or packages.
-
\item @{command (global) "end"} concludes the current theory
definition. Note that some other commands, e.g.\ local theory
targets @{command locale} or @{command class} may involve a
--- a/src/Pure/System/build.ML Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Pure/System/build.ML Tue Sep 11 11:53:34 2012 +0200
@@ -71,6 +71,12 @@
(case duplicates (op =) (map fst document_variants) of
[] => ()
| dups => error ("Duplicate document variants: " ^ commas_quote dups));
+
+ val _ =
+ if Options.string options "document_dump" = "" then ()
+ else
+ Output.physical_stderr
+ "### Legacy feature: old option \"document_dump\" -- use \"document_output\" instead\n";
val _ =
Session.init do_output false
(Options.bool options "browser_info") browser_info
--- a/src/Pure/System/options.scala Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Pure/System/options.scala Tue Sep 11 11:53:34 2012 +0200
@@ -7,6 +7,7 @@
package isabelle
+import java.util.Locale
import java.util.Calendar
@@ -21,16 +22,21 @@
sealed abstract class Type
{
- def print: String = toString.toLowerCase
+ def print: String = toString.toLowerCase(Locale.ENGLISH)
}
- private case object Bool extends Type
- private case object Int extends Type
- private case object Real extends Type
- private case object String extends Type
- private case object Unknown extends Type
+ 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
- case class Opt(typ: Type, value: String, description: String)
+ case class Opt(name: String, typ: Type, value: String, description: String)
{
+ def print: String =
+ "option " + name + " : " + typ.print + " = " +
+ (if (typ == Options.String) quote(value) else value) +
+ (if (description == "") "" else "\n -- " + quote(description))
+
def unknown: Boolean = typ == Unknown
}
@@ -123,16 +129,26 @@
{
override def toString: String = options.iterator.mkString("Options (", ",", ")")
- def print: String =
- cat_lines(options.toList.sortBy(_._1).map({ case (name, opt) =>
- "option " + name + " : " + opt.typ.print + " = " +
- (if (opt.typ == Options.String) quote(opt.value) else opt.value) +
- (if (opt.description == "") "" else "\n -- " + quote(opt.description)) }))
+ def print: String = cat_lines(options.toList.sortBy(_._1).map(p => p._2.print))
+
+ def title(strip: String, name: String): String =
+ {
+ check_name(name)
+ val words = space_explode('_', name)
+ val words1 =
+ words match {
+ case word :: rest if word == strip => rest
+ case _ => words
+ }
+ words1.map(Library.capitalize).mkString(" ")
+ }
+
+ def description(name: String): String = check_name(name).description
/* check */
- private def check_name(name: String): Options.Opt =
+ def check_name(name: String): Options.Opt =
options.get(name) match {
case Some(opt) if !opt.unknown => opt
case _ => error("Unknown option " + quote(name))
@@ -223,7 +239,7 @@
case "string" => Options.String
case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
}
- val opt = Options.Opt(typ, value, description)
+ val opt = Options.Opt(name, typ, value, description)
(new Options(options + (name -> opt))).check_value(name)
}
}
@@ -231,7 +247,7 @@
def add_permissive(name: String, value: String): Options =
{
if (options.isDefinedAt(name)) this + (name, value)
- else new Options(options + (name -> Options.Opt(Options.Unknown, value, "")))
+ else new Options(options + (name -> Options.Opt(name, Options.Unknown, value, "")))
}
def + (name: String, value: String): Options =
@@ -302,3 +318,64 @@
"(* generated by Isabelle " + Calendar.getInstance.getTime + " *)\n\n" + prefs)
}
}
+
+
+class Options_Variable
+{
+ // owned by Swing thread
+ @volatile private var options = Options.empty
+
+ def value: Options = options
+ def update(new_options: Options)
+ {
+ Swing_Thread.require()
+ options = new_options
+ }
+
+ def + (name: String, x: String)
+ {
+ Swing_Thread.require()
+ options = options + (name, x)
+ }
+
+ val bool = new Object
+ {
+ def apply(name: String): Boolean = options.bool(name)
+ def update(name: String, x: Boolean)
+ {
+ Swing_Thread.require()
+ options = options.bool.update(name, x)
+ }
+ }
+
+ val int = new Object
+ {
+ def apply(name: String): Int = options.int(name)
+ def update(name: String, x: Int)
+ {
+ Swing_Thread.require()
+ options = options.int.update(name, x)
+ }
+ }
+
+ val real = new Object
+ {
+ def apply(name: String): Double = options.real(name)
+ def update(name: String, x: Double)
+ {
+ Swing_Thread.require()
+ options = options.real.update(name, x)
+ }
+ }
+
+ val string = new Object
+ {
+ def apply(name: String): String = options.string(name)
+ def update(name: String, x: String)
+ {
+ Swing_Thread.require()
+ options = options.string.update(name, x)
+ }
+ }
+}
+
--- a/src/Pure/System/session.ML Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Pure/System/session.ML Tue Sep 11 11:53:34 2012 +0200
@@ -121,7 +121,9 @@
name dump rpath level timing verbose max_threads trace_threads
parallel_proofs parallel_proofs_threshold =
((fn () =>
- (init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
+ (Output.physical_stderr
+ "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
+ init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
(doc_dump dump) rpath verbose;
with_timing item timing use root;
finish ()))
--- a/src/Pure/System/session.scala Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Pure/System/session.scala Tue Sep 11 11:53:34 2012 +0200
@@ -52,7 +52,6 @@
val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement)
val output_delay = Time.seconds(0.1) // prover output (markup, common messages)
val update_delay = Time.seconds(0.5) // GUI layout updates
- val load_delay = Time.seconds(0.5) // file load operations (new buffers etc.)
val prune_delay = Time.seconds(60.0) // prune history -- delete old versions
val prune_size = 0 // size of retained history
val syslog_limit = 100
--- a/src/Pure/System/swing_thread.scala Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Pure/System/swing_thread.scala Tue Sep 11 11:53:34 2012 +0200
@@ -54,14 +54,14 @@
def postpone(time: Time): Unit
}
- private def delayed_action(first: Boolean)(time: Time)(action: => Unit): Delay =
+ private def delayed_action(first: Boolean)(time: => Time)(action: => Unit): Delay =
new Delay {
private val timer = new Timer(time.ms.toInt, null)
timer.setRepeats(false)
timer.addActionListener(new ActionListener {
override def actionPerformed(e: ActionEvent) {
assert()
- timer.setDelay(time.ms.toInt)
+ timer.setInitialDelay(time.ms.toInt)
action
}
})
@@ -76,14 +76,14 @@
{
require()
timer.stop()
- timer.setDelay(time.ms.toInt)
+ timer.setInitialDelay(time.ms.toInt)
}
def postpone(alt_time: Time)
{
require()
if (timer.isRunning) {
- timer.setDelay(timer.getDelay max alt_time.ms.toInt)
+ timer.setInitialDelay(timer.getInitialDelay max alt_time.ms.toInt)
timer.restart()
}
}
--- a/src/Pure/Thy/thy_load.ML Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML Tue Sep 11 11:53:34 2012 +0200
@@ -273,6 +273,22 @@
in (thy, present) end;
+(* document antiquotation *)
+
+val _ =
+ Context.>> (Context.map_theory
+ (Thy_Output.antiquotation (Binding.name "file") (Scan.lift (Parse.position Parse.path))
+ (fn {context = ctxt, ...} => fn (name, pos) =>
+ let
+ val dir = master_directory (Proof_Context.theory_of ctxt);
+ val path = Path.append dir (Path.explode name);
+ val _ =
+ if File.exists path then ()
+ else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
+ val _ = Position.report pos (Isabelle_Markup.path name);
+ in Thy_Output.verb_text name end)));
+
+
(* global master path *)
local
--- a/src/Pure/Thy/thy_output.ML Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Sep 11 11:53:34 2012 +0200
@@ -42,6 +42,7 @@
val maybe_pretty_source: (Proof.context -> 'a -> Pretty.T) -> Proof.context ->
Args.src -> 'a list -> Pretty.T list
val output: Proof.context -> Pretty.T list -> string
+ val verb_text: string -> string
end;
structure Thy_Output: THY_OUTPUT =
@@ -685,14 +686,4 @@
end;
-
-(* files *)
-
-val _ =
- Context.>> (Context.map_theory
- (antiquotation (Binding.name "file") (Scan.lift Args.name)
- (fn _ => fn path =>
- if File.exists (Path.explode path) then verb_text path
- else error ("Bad file: " ^ quote path))));
-
end;
--- a/src/Pure/library.scala Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Pure/library.scala Tue Sep 11 11:53:34 2012 +0200
@@ -9,6 +9,7 @@
import java.lang.System
+import java.util.Locale
import java.awt.Component
import javax.swing.JOptionPane
@@ -84,6 +85,10 @@
if (str.endsWith("\n")) str.substring(0, str.length - 1)
else str
+ def capitalize(str: String): String =
+ if (str.length == 0) str
+ else str.substring(0, 1).toUpperCase(Locale.ENGLISH) + str.substring(1)
+
/* quote */
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/etc/options Tue Sep 11 11:53:34 2012 +0200
@@ -0,0 +1,22 @@
+(* :mode=isabelle-options: *)
+
+option jedit_logic : string = ""
+ -- "default logic session"
+
+option jedit_auto_start : bool = true
+ -- "auto-start prover session on editor startup"
+
+option jedit_relative_font_size : int = 100
+ -- "relative font size of output panel wrt. main text area"
+
+option jedit_tooltip_font_size : int = 10
+ -- "tooltip font size (according to HTML)"
+
+option jedit_tooltip_margin : int = 60
+ -- "margin for tooltip pretty-printing"
+
+option jedit_tooltip_dismiss_delay : real = 8.0
+ -- "global delay for Swing tooltips"
+
+option jedit_load_delay : real = 0.5
+ -- "delay for file load operations (new buffers etc.)"
--- a/src/Tools/jEdit/lib/Tools/jedit Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue Sep 11 11:53:34 2012 +0200
@@ -14,10 +14,12 @@
"src/html_panel.scala"
"src/hyperlink.scala"
"src/isabelle_encoding.scala"
+ "src/isabelle_logic.scala"
"src/isabelle_options.scala"
"src/isabelle_rendering.scala"
"src/isabelle_sidekick.scala"
"src/jedit_thy_load.scala"
+ "src/jedit_options.scala"
"src/output_dockable.scala"
"src/plugin.scala"
"src/protocol_dockable.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Tue Sep 11 11:53:34 2012 +0200
@@ -23,17 +23,6 @@
plugin.isabelle.jedit.Plugin.option-pane=isabelle
options.isabelle.label=Isabelle
options.isabelle.code=new isabelle.jedit.Isabelle_Options();
-options.isabelle.logic.title=Logic
-options.isabelle.relative-font-size.title=Relative Font Size
-options.isabelle.relative-font-size=100
-options.isabelle.tooltip-font-size.title=Tooltip Font Size
-options.isabelle.tooltip-font-size=10
-options.isabelle.tooltip-margin.title=Tooltip Margin
-options.isabelle.tooltip-margin=60
-options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
-options.isabelle.tooltip-dismiss-delay=8.0
-options.isabelle.auto-start.title=Auto Start
-options.isabelle.auto-start=true
#actions
isabelle.check-buffer.label=Commence full proof checking of current buffer
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Tue Sep 11 11:53:34 2012 +0200
@@ -0,0 +1,78 @@
+/* Title: Tools/jEdit/src/isabelle_logic.scala
+ Author: Makarius
+
+Isabellel logic session.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.swing.ComboBox
+import scala.swing.event.SelectionChanged
+
+
+object Isabelle_Logic
+{
+ private def default_logic(): String =
+ {
+ val logic = Isabelle_System.getenv("JEDIT_LOGIC")
+ if (logic != "") logic
+ else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
+ }
+
+ private class Logic_Entry(val name: String, val description: String)
+ {
+ override def toString = description
+ }
+
+ def logic_selector(autosave: Boolean): Option_Component =
+ {
+ Swing_Thread.require()
+
+ val entries =
+ new Logic_Entry("", "default (" + default_logic() + ")") ::
+ Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
+
+ val component = new ComboBox(entries) with Option_Component {
+ val title = Isabelle.options.title("jedit_logic")
+ def load: Unit =
+ {
+ val logic = Isabelle.options.string("jedit_logic")
+ entries.find(_.name == logic) match {
+ case Some(entry) => selection.item = entry
+ case None =>
+ }
+ }
+ def save: Unit = Isabelle.options.string("jedit_logic") = selection.item.name
+ }
+
+ component.load()
+ if (autosave) {
+ component.listenTo(component.selection)
+ component.reactions += { case SelectionChanged(_) => component.save() }
+ }
+ component.tooltip = Isabelle.tooltip(Isabelle.options.value.check_name("jedit_logic").print)
+ component
+ }
+
+ def session_args(): List[String] =
+ {
+ val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
+ val logic =
+ Isabelle.options.string("jedit_logic") match {
+ case "" => default_logic()
+ case logic => logic
+ }
+ modes ::: List(logic)
+ }
+
+ def session_content(inlined_files: Boolean): Build.Session_Content =
+ {
+ val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
+ val name = Path.explode(session_args().last).base.implode // FIXME more robust
+ Build.session_content(inlined_files, dirs, name).check_errors
+ }
+}
+
--- a/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala Tue Sep 11 11:53:34 2012 +0200
@@ -1,5 +1,5 @@
/* Title: Tools/jEdit/src/isabelle_options.scala
- Author: Johannes Hölzl, TU Munich
+ Author: Makarius
Editor pane for plugin options.
*/
@@ -9,60 +9,27 @@
import isabelle._
-import javax.swing.JSpinner
-
-import scala.swing.CheckBox
-
import org.gjt.sp.jedit.AbstractOptionPane
class Isabelle_Options extends AbstractOptionPane("isabelle")
{
- private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
- private val auto_start = new CheckBox()
- private val relative_font_size = new JSpinner()
- private val tooltip_font_size = new JSpinner()
- private val tooltip_margin = new JSpinner()
- private val tooltip_dismiss_delay = new JSpinner()
+ private val components = List(
+ Isabelle_Logic.logic_selector(false),
+ Isabelle.options.make_component("jedit_auto_start"),
+ Isabelle.options.make_component("jedit_relative_font_size"),
+ Isabelle.options.make_component("jedit_tooltip_font_size"),
+ Isabelle.options.make_component("jedit_tooltip_margin"),
+ Isabelle.options.make_component("jedit_tooltip_dismiss_delay"),
+ Isabelle.options.make_component("jedit_load_delay"))
override def _init()
{
- addComponent(Isabelle.Property("logic.title"),
- logic_selector.peer.asInstanceOf[java.awt.Component])
-
- addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
- auto_start.selected = Isabelle.Boolean_Property("auto-start")
-
- relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
- addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
-
- tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
- addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
-
- tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
- addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
-
- tooltip_dismiss_delay.setValue(
- Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt)
- addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
+ for (c <- components) addComponent(c.title, c.peer)
}
override def _save()
{
- Isabelle.Property("logic") = logic_selector.selection.item.name
-
- Isabelle.Boolean_Property("auto-start") = auto_start.selected
-
- Isabelle.Int_Property("relative-font-size") =
- relative_font_size.getValue().asInstanceOf[Int]
-
- Isabelle.Int_Property("tooltip-font-size") =
- tooltip_font_size.getValue().asInstanceOf[Int]
-
- Isabelle.Int_Property("tooltip-margin") =
- tooltip_margin.getValue().asInstanceOf[Int]
-
- Isabelle.Time_Property("tooltip-dismiss-delay") =
- Time.ms(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
+ for (c <- components) c.save()
}
}
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Tue Sep 11 11:53:34 2012 +0200
@@ -151,7 +151,7 @@
private def tooltip_text(msg: XML.Tree): String =
- Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
+ Pretty.string_of(List(msg), margin = Isabelle.options.int("jedit_tooltip_margin"))
def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
{
@@ -195,7 +195,7 @@
private def string_of_typing(kind: String, body: XML.Body): String =
Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
- margin = Isabelle.Int_Property("tooltip-margin"))
+ margin = Isabelle.options.int("jedit_tooltip_margin"))
def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
{
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_options.scala Tue Sep 11 11:53:34 2012 +0200
@@ -0,0 +1,68 @@
+/* Title: Tools/jEdit/src/jedit_options.scala
+ Author: Makarius
+
+Options for Isabelle/jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import javax.swing.{InputVerifier, JComponent, UIManager}
+import javax.swing.text.JTextComponent
+
+import scala.swing.{Component, CheckBox, TextArea}
+
+
+trait Option_Component extends Component
+{
+ val title: String
+ def load(): Unit
+ def save(): Unit
+}
+
+class JEdit_Options extends Options_Variable
+{
+ def title(opt_name: String): String = value.title("jedit", opt_name)
+
+ def make_component(opt_name: String): Option_Component =
+ {
+ Swing_Thread.require()
+
+ val opt = value.check_name(opt_name)
+ val opt_title = title(opt_name)
+
+ val component =
+ if (opt.typ == Options.Bool)
+ new CheckBox with Option_Component {
+ val title = opt_title
+ def load = selected = bool(opt_name)
+ def save = bool(opt_name) = selected
+ }
+ else {
+ val default_font = UIManager.getFont("TextField.font")
+ val text_area =
+ new TextArea with Option_Component {
+ if (default_font != null) font = default_font
+ val title = opt_title
+ def load = text = value.check_name(opt_name).value
+ def save = update(value + (opt_name, text))
+ }
+ text_area.peer.setInputVerifier(new InputVerifier {
+ def verify(jcomponent: JComponent): Boolean =
+ jcomponent match {
+ case text: JTextComponent =>
+ try { value + (opt_name, text.getText); true }
+ catch { case ERROR(_) => false }
+ case _ => true
+ }
+ })
+ text_area
+ }
+ component.load()
+ component.tooltip = Isabelle.tooltip(opt.print)
+ component
+ }
+}
+
--- a/src/Tools/jEdit/src/plugin.scala Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Sep 11 11:53:34 2012 +0200
@@ -14,7 +14,7 @@
import javax.swing.JOptionPane
import scala.collection.mutable
-import scala.swing.{ComboBox, ListView, ScrollPane}
+import scala.swing.{ListView, ScrollPane}
import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
Buffer, EditPane, ServiceManager, View}
@@ -34,6 +34,8 @@
{
/* plugin instance */
+ val options = new JEdit_Options
+
@volatile var startup_failure: Option[Throwable] = None
@volatile var startup_notified = false
@@ -51,81 +53,26 @@
}
- /* properties */
-
- val OPTION_PREFIX = "options.isabelle."
-
- object Property
- {
- def apply(name: String): String =
- jEdit.getProperty(OPTION_PREFIX + name)
- def apply(name: String, default: String): String =
- jEdit.getProperty(OPTION_PREFIX + name, default)
- def update(name: String, value: String) =
- jEdit.setProperty(OPTION_PREFIX + name, value)
- }
-
- object Boolean_Property
- {
- def apply(name: String): Boolean =
- jEdit.getBooleanProperty(OPTION_PREFIX + name)
- def apply(name: String, default: Boolean): Boolean =
- jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
- def update(name: String, value: Boolean) =
- jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
- }
-
- object Int_Property
- {
- def apply(name: String): Int =
- jEdit.getIntegerProperty(OPTION_PREFIX + name)
- def apply(name: String, default: Int): Int =
- jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
- def update(name: String, value: Int) =
- jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
- }
-
- object Double_Property
- {
- def apply(name: String): Double =
- jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
- def apply(name: String, default: Double): Double =
- jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
- def update(name: String, value: Double) =
- jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
- }
-
- object Time_Property
- {
- def apply(name: String): Time =
- Time.seconds(Double_Property(name))
- def apply(name: String, default: Time): Time =
- Time.seconds(Double_Property(name, default.seconds))
- def update(name: String, value: Time) =
- Double_Property.update(name, value.seconds)
- }
-
-
/* font */
def font_family(): String = jEdit.getProperty("view.font")
def font_size(): Float =
(jEdit.getIntegerProperty("view.fontsize", 16) *
- Int_Property("relative-font-size", 100)).toFloat / 100
+ options.int("jedit_relative_font_size")).toFloat / 100
/* tooltip markup */
def tooltip(text: String): String =
"<html><pre style=\"font-family: " + font_family() + "; font-size: " +
- Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?)
+ options.int("jedit_tooltip_font_size").toString + "px; \">" + // FIXME proper scaling (!?)
HTML.encode(text) + "</pre></html>"
private val tooltip_lb = Time.seconds(0.5)
private val tooltip_ub = Time.seconds(60.0)
def tooltip_dismiss_delay(): Time =
- Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub
+ Time.seconds(options.real("jedit_tooltip_dismiss_delay")) max tooltip_lb min tooltip_ub
def setup_tooltips()
{
@@ -280,53 +227,6 @@
}
- /* logic image */
-
- def default_logic(): String =
- {
- val logic = Isabelle_System.getenv("JEDIT_LOGIC")
- if (logic != "") logic
- else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
- }
-
- class Logic_Entry(val name: String, val description: String)
- {
- override def toString = description
- }
-
- def logic_selector(logic: String): ComboBox[Logic_Entry] =
- {
- val entries =
- new Logic_Entry("", "default (" + default_logic() + ")") ::
- Isabelle_System.find_logics().map(name => new Logic_Entry(name, name))
- val component = new ComboBox(entries)
- entries.find(_.name == logic) match {
- case None =>
- case Some(entry) => component.selection.item = entry
- }
- component.tooltip = "Isabelle logic image"
- component
- }
-
- def session_args(): List[String] =
- {
- val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
- val logic = {
- val logic = Property("logic")
- if (logic != null && logic != "") logic
- else Isabelle.default_logic()
- }
- modes ::: List(logic)
- }
-
- def session_content(inlined_files: Boolean): Build.Session_Content =
- {
- val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS"))
- val name = Path.explode(session_args().last).base.implode // FIXME more robust
- Build.session_content(inlined_files, dirs, name).check_errors
- }
-
-
/* convenience actions */
private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
@@ -361,7 +261,7 @@
/* theory files */
private lazy val delay_load =
- Swing_Thread.delay_last(Isabelle.session.load_delay)
+ Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("jedit_load_delay")))
{
val view = jEdit.getActiveView()
@@ -450,8 +350,8 @@
if (Isabelle.startup_failure.isEmpty) {
message match {
case msg: EditorStarted =>
- if (Isabelle.Boolean_Property("auto-start"))
- Isabelle.session.start(Isabelle.session_args())
+ if (Isabelle.options.bool("jedit_auto_start"))
+ Isabelle.session.start(Isabelle_Logic.session_args())
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
@@ -492,15 +392,20 @@
{
try {
Isabelle.plugin = this
- Isabelle.setup_tooltips()
Isabelle_System.init()
Isabelle_System.install_fonts()
+ val init_options = Options.init()
+ Swing_Thread.now {
+ Isabelle.options.update(init_options)
+ Isabelle.setup_tooltips()
+ }
+
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
if (ModeProvider.instance.isInstanceOf[ModeProvider])
ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
- val content = Isabelle.session_content(false)
+ val content = Isabelle_Logic.session_content(false)
val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
Isabelle.session = new Session(thy_load)
@@ -516,6 +421,9 @@
override def stop()
{
+ if (Isabelle.startup_failure.isEmpty)
+ Isabelle.options.value.save_prefs()
+
Isabelle.session.phase_changed -= session_manager
Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
Isabelle.session.stop()
--- a/src/Tools/jEdit/src/session_dockable.scala Tue Sep 11 09:40:05 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Tue Sep 11 11:53:34 2012 +0200
@@ -11,7 +11,7 @@
import scala.actors.Actor._
import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
-import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged}
+import scala.swing.event.{ButtonClicked, MouseClicked}
import java.lang.System
import java.awt.{BorderLayout, Graphics2D, Insets}
@@ -60,11 +60,7 @@
}
check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
- private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
- logic.listenTo(logic.selection)
- logic.reactions += {
- case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
- }
+ private val logic = Isabelle_Logic.logic_selector(true)
private val controls =
new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
@@ -154,6 +150,8 @@
react {
case phase: Session.Phase => handle_phase(phase)
+ case Session.Global_Settings => Swing_Thread.later { logic.load () }
+
case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
@@ -164,12 +162,14 @@
override def init()
{
Isabelle.session.phase_changed += main_actor; handle_phase(Isabelle.session.phase)
+ Isabelle.session.global_settings += main_actor
Isabelle.session.commands_changed += main_actor; handle_update()
}
override def exit()
{
Isabelle.session.phase_changed -= main_actor
+ Isabelle.session.global_settings -= main_actor
Isabelle.session.commands_changed -= main_actor
}
}