# HG changeset patch
# User wenzelm
# Date 1347357214 -7200
# Node ID 7157af98ca550d70e86e3b4239ae1114153cd66a
# Parent  9e9dd498fb230e6283e8054c7c14342eb2ee8b10# Parent  9e10481dd3c40aa240621d9d7e18f409ada5e5bf
merged

diff -r 9e9dd498fb23 -r 7157af98ca55 NEWS
--- 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.
 
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Doc/IsarRef/Spec.thy
--- 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
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Pure/System/build.ML
--- 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
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Pure/System/options.scala
--- 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)
+    }
+  }
+}
+
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Pure/System/session.ML
--- 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 ()))
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Pure/System/session.scala
--- 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
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Pure/System/swing_thread.scala
--- 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()
         }
       }
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Pure/Thy/thy_load.ML
--- 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
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Pure/Thy/thy_output.ML
--- 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;
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Pure/library.scala
--- 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 */
 
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Tools/jEdit/etc/options
--- /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.)"
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Tools/jEdit/lib/Tools/jedit
--- 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"
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Tools/jEdit/src/Isabelle.props
--- 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
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Tools/jEdit/src/isabelle_logic.scala
--- /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
+  }
+}
+
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Tools/jEdit/src/isabelle_options.scala
--- 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()
   }
 }
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Tools/jEdit/src/isabelle_rendering.scala
--- 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] =
   {
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Tools/jEdit/src/jedit_options.scala
--- /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
+  }
+}
+
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Tools/jEdit/src/plugin.scala
--- 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()
diff -r 9e9dd498fb23 -r 7157af98ca55 src/Tools/jEdit/src/session_dockable.scala
--- 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
   }
 }