Custom Query (361 matches)

The preference mechanism should support dynamically computed defaults. This can be achieved by using reflection together with a method name given in the preference file:

 <pref name="ActiveHighlight" type="string" setDefault="setExample"/>

The method should be located in the already given class associated with the preference file, e.g. ExamplePrefs.java:

  public Boolean setExample() {
     return Eclipse.isRunningOnMac() ? "Orange" : "Blue";
  }

This is bogus and slightly silly example, but one reason we want this is to set platform-specific defaults for some values.

See Pure/ProofGeneral?/parsing.ML.

This is an absolutely essential improvement required for Isabelle2007 to have good PGIP support.

The current Isabelle CVS version displays goals correctly but double-escapes the XML in terms when it prints theorems.

Test case: run isabelle -I -X and paste in the following two PGIP lines:

<pgip class="pa" id="test" seq="1"><opentheory thyname="SymbolOutput" parentnames="Main">theory SymbolOutput imports Main
begin</opentheory></pgip>

<pgip class="pa" id="test" seq="2"><spuriouscmd>thm trancl_def</spuriouscmd></pgip>

the output should contain text like this:

<pgmltext>trancl <sym name="equiv">&lt;equiv;&gt;</sym>;equiv;&gt;</sym>

and not text like this:

<pgmltext>trancl &lt;sym name = &quot;equiv&quot;&gt;\&amp;lt;equiv&amp;gt;&lt;/sym&gt;

which has too much escaping. The goals output does the right thing, e.g. try this PGIP command:

<pgip class="pa" id="test" seq="3"><opengoal>lemma "P \&lt;equiv&gt; P"</opengoal></pgip>

which gives PGML text containing:

goal (1 subgoal):
 1. <atom kind = "free">P</atom> <sym name = "equiv">\&lt;equiv&gt;</sym>