--- a/Admin/isatest/settings/cygwin-poly-e Tue Jun 01 17:25:00 2010 +0200
+++ b/Admin/isatest/settings/cygwin-poly-e Wed Jun 02 08:01:45 2010 +0200
@@ -1,6 +1,6 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/isatest/homebroy/home/polyml/polyml-5.3.0"
+ POLYML_HOME="/home/isatest/polyml-5.3.0"
ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86-cygwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
--- a/src/Pure/General/secure.ML Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/General/secure.ML Wed Jun 02 08:01:45 2010 +0200
@@ -13,7 +13,8 @@
val use_text: use_context -> int * string -> bool -> string -> unit
val use_file: use_context -> bool -> string -> unit
val toplevel_pp: string list -> string -> unit
- val open_unsynchronized: unit -> unit
+ val Isar_setup: unit -> unit
+ val PG_setup: unit -> unit
val commit: unit -> unit
val bash_output: string -> string * int
val bash: string -> int
@@ -54,7 +55,9 @@
val use_global = raw_use_text ML_Parse.global_context (0, "") false;
fun commit () = use_global "commit();"; (*commit is dynamically bound!*)
-fun open_unsynchronized () = use_global "open Unsynchronized";
+
+fun Isar_setup () = use_global "open Unsynchronized;";
+fun PG_setup () = use_global "structure ThyLoad = Thy_Load;";
(* shell commands *)
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Jun 02 08:01:45 2010 +0200
@@ -245,6 +245,7 @@
Unsynchronized.set initialized);
sync_thy_loader ();
Unsynchronized.change print_mode (update (op =) proof_generalN);
+ Secure.PG_setup ();
Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
end;
--- a/src/Pure/ROOT.ML Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/ROOT.ML Wed Jun 02 08:01:45 2010 +0200
@@ -305,11 +305,9 @@
structure PrintMode = Print_Mode;
structure SpecParse = Parse_Spec;
structure ThyInfo = Thy_Info;
+structure ThyLoad = Thy_Load;
structure ThyOutput = Thy_Output;
structure TypeInfer = Type_Infer;
end;
-structure ThyLoad = Thy_Load; (*Proof General legacy*)
-
-
--- a/src/Pure/System/isar.ML Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/System/isar.ML Wed Jun 02 08:01:45 2010 +0200
@@ -138,7 +138,7 @@
fun toplevel_loop {init = do_init, welcome, sync, secure} =
(Context.set_thread_data NONE;
- Secure.open_unsynchronized ();
+ Secure.Isar_setup ();
if do_init then init () else ();
if welcome then writeln (Session.welcome ()) else ();
uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar sync)) ());
--- a/src/Pure/display.ML Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/display.ML Wed Jun 02 08:01:45 2010 +0200
@@ -129,7 +129,7 @@
fun prt_cls c = Syntax.pretty_sort ctxt [c];
fun prt_sort S = Syntax.pretty_sort ctxt S;
- fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
+ fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
--- a/src/Pure/sorts.ML Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Pure/sorts.ML Wed Jun 02 08:01:45 2010 +0200
@@ -26,7 +26,7 @@
val insert_terms: term list -> sort OrdList.T -> sort OrdList.T
type algebra
val classes_of: algebra -> serial Graph.T
- val arities_of: algebra -> (class * (class * sort list)) list Symtab.table
+ val arities_of: algebra -> (class * sort list) list Symtab.table
val all_classes: algebra -> class list
val super_classes: algebra -> class -> class list
val class_less: algebra -> class * class -> bool
@@ -105,15 +105,14 @@
arities: table of association lists of all type arities; (t, ars)
means that type constructor t has the arities ars; an element
- (c, (c0, Ss)) of ars represents the arity t::(Ss)c being derived
- via c0 <= c. "Coregularity" of the arities structure requires
- that for any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that
- c1 <= c2 holds Ss1 <= Ss2.
+ (c, Ss) of ars represents the arity t::(Ss)c. "Coregularity" of
+ the arities structure requires that for any two declarations
+ t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2.
*)
datatype algebra = Algebra of
{classes: serial Graph.T,
- arities: (class * (class * sort list)) list Symtab.table};
+ arities: (class * sort list) list Symtab.table};
fun classes_of (Algebra {classes, ...}) = classes;
fun arities_of (Algebra {arities, ...}) = arities;
@@ -225,9 +224,9 @@
Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^
Pretty.string_of_arity pp (t, Ss', [c']));
-fun coregular pp algebra t (c, (c0, Ss)) ars =
+fun coregular pp algebra t (c, Ss) ars =
let
- fun conflict (c', (_, Ss')) =
+ fun conflict (c', Ss') =
if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then
SOME ((c, c'), (c', Ss'))
else if class_le algebra (c', c) andalso not (sorts_le algebra (Ss', Ss)) then
@@ -236,19 +235,18 @@
in
(case get_first conflict ars of
SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss')
- | NONE => (c, (c0, Ss)) :: ars)
+ | NONE => (c, Ss) :: ars)
end;
-fun complete algebra (c0, Ss) = map (rpair (c0, Ss)) (c0 :: super_classes algebra c0);
+fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c);
-fun insert pp algebra t (c, (c0, Ss)) ars =
+fun insert pp algebra t (c, Ss) ars =
(case AList.lookup (op =) ars c of
- NONE => coregular pp algebra t (c, (c0, Ss)) ars
- | SOME (_, Ss') =>
+ NONE => coregular pp algebra t (c, Ss) ars
+ | SOME Ss' =>
if sorts_le algebra (Ss, Ss') then ars
- else if sorts_le algebra (Ss', Ss) then
- coregular pp algebra t (c, (c0, Ss))
- (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars)
+ else if sorts_le algebra (Ss', Ss)
+ then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars)
else err_conflict pp t NONE (c, Ss) (c, Ss'));
in
@@ -265,7 +263,7 @@
algebra |> map_arities (insert_complete_ars pp algebra arg);
fun add_arities_table pp algebra =
- Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars));
+ Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars));
end;
@@ -310,16 +308,17 @@
in make_algebra (classes', arities') end;
-(* algebra projections *)
+(* algebra projections *) (* FIXME potentially violates abstract type integrity *)
fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) =
let
val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
- fun restrict_arity tyco (c, (_, Ss)) =
- if P c then case sargs (c, tyco)
- of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
- |> map restrict_sort))
- | NONE => NONE
+ fun restrict_arity t (c, Ss) =
+ if P c then
+ (case sargs (c, t) of
+ SOME sorts =>
+ SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort)
+ | NONE => NONE)
else NONE;
val classes' = classes |> Graph.subgraph P;
val arities' = arities |> Symtab.map' (map_filter o restrict_arity);
@@ -355,7 +354,7 @@
fun dom c =
(case AList.lookup (op =) (Symtab.lookup_list arities a) c of
NONE => raise CLASS_ERROR (No_Arity (a, c))
- | SOME (_, Ss) => Ss);
+ | SOME Ss => Ss);
fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss);
in
(case S of
@@ -380,11 +379,8 @@
in uncurry meet end;
fun meet_sort_typ algebra (T, S) =
- let
- val tab = meet_sort algebra (T, S) Vartab.empty;
- in Term.map_type_tvar (fn (v, _) =>
- TVar (v, (the o Vartab.lookup tab) v))
- end;
+ let val tab = meet_sort algebra (T, S) Vartab.empty;
+ in Term.map_type_tvar (fn (v, _) => TVar (v, (the o Vartab.lookup tab) v)) end;
(* of_sort *)
@@ -425,9 +421,9 @@
in
S |> map (fn c =>
let
- val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
+ val Ss' = the (AList.lookup (op =) (Symtab.lookup_list arities a) c);
val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss');
- in class_relation T (type_constructor (a, Us) dom' c0, c0) c end)
+ in type_constructor (a, Us) dom' c end)
end
| derive (T, S) = weaken T (type_variable T) S;
in derive end;
--- a/src/Tools/jEdit/src/jedit/document_view.scala Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Jun 02 08:01:45 2010 +0200
@@ -19,6 +19,7 @@
import org.gjt.sp.jedit.gui.RolloverButton
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.syntax.SyntaxStyle
object Document_View
@@ -78,6 +79,24 @@
private val session = model.session
+ /* extended token styles */
+
+ private var styles: Array[SyntaxStyle] = null // owned by Swing thread
+
+ def extend_styles()
+ {
+ Swing_Thread.assert()
+ styles = Isabelle_Token_Marker.extend_styles(text_area.getPainter.getStyles)
+ }
+ extend_styles()
+
+ def set_styles()
+ {
+ Swing_Thread.assert()
+ text_area.getPainter.setStyles(styles)
+ }
+
+
/* commands_changed_actor */
private val commands_changed_actor = actor {
--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Wed Jun 02 08:01:45 2010 +0200
@@ -11,13 +11,46 @@
import isabelle._
import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, ParserRuleSet}
+import org.gjt.sp.jedit.syntax.{Token, TokenMarker, TokenHandler, ParserRuleSet, SyntaxStyle}
+import org.gjt.sp.jedit.textarea.TextArea
+import java.awt.Font
+import java.awt.font.TextAttribute
import javax.swing.text.Segment;
object Isabelle_Token_Marker
{
+ /* extended token styles */
+
+ private val plain_range: Int = Token.ID_COUNT
+ private val full_range: Int = 3 * plain_range
+ private def check_range(i: Int) { require(0 <= i && i < plain_range) }
+
+ def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
+ def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
+
+ private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
+ {
+ import scala.collection.JavaConversions._
+ val script_font =
+ style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
+ new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
+ }
+
+ def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
+ {
+ val new_styles = new Array[SyntaxStyle](full_range)
+ for (i <- 0 until plain_range) {
+ val style = styles(i)
+ new_styles(i) = style
+ new_styles(subscript(i.toByte)) = script_style(style, -1)
+ new_styles(superscript(i.toByte)) = script_style(style, 1)
+ }
+ new_styles
+ }
+
+
/* line context */
private val rule_set = new ParserRuleSet("isabelle", "MAIN")
@@ -122,6 +155,13 @@
def to: Int => Int = model.to_current(document, _)
def from: Int => Int = model.from_current(document, _)
+ for (text_area <- Isabelle.jedit_text_areas(model.buffer)
+ if Document_View(text_area).isDefined)
+ Document_View(text_area).get.set_styles()
+
+ def handle_token(style: Byte, offset: Int, length: Int) =
+ handler.handleToken(line_segment, style, offset, length, context)
+
var next_x = start
for {
(command, command_start) <- document.command_range(from(start), from(stop))
@@ -137,7 +177,7 @@
((abs_stop - stop) max 0)
}
{
- val byte =
+ val token_type =
markup.info match {
case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
Isabelle_Token_Marker.command_style(kind)
@@ -146,15 +186,14 @@
case _ => Token.NULL
}
if (start + token_start > next_x)
- handler.handleToken(line_segment, 1,
- next_x - start, start + token_start - next_x, context)
- handler.handleToken(line_segment, byte, token_start, token_length, context)
+ handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
+ handle_token(token_type, token_start, token_length)
next_x = start + token_start + token_length
}
if (next_x < stop)
- handler.handleToken(line_segment, 1, next_x - start, stop - next_x, context)
+ handle_token(Token.COMMENT1, next_x - start, stop - next_x)
- handler.handleToken(line_segment, Token.END, line_segment.count, 0, context)
+ handle_token(Token.END, line_segment.count, 0)
handler.setLineContext(context)
context
}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Tue Jun 01 17:25:00 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Wed Jun 02 08:01:45 2010 +0200
@@ -228,6 +228,11 @@
}
case msg: PropertiesChanged =>
+ Swing_Thread.now {
+ for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
+ Document_View(text_area).get.extend_styles()
+ }
+
Isabelle.session.global_settings.event(Session.Global_Settings)
case _ =>