--- a/src/Pure/General/symbol_pos.ML Wed Dec 12 15:38:47 2012 +0100
+++ b/src/Pure/General/symbol_pos.ML Wed Dec 12 19:03:49 2012 +0100
@@ -37,7 +37,6 @@
val range: T list -> Position.range
val implode_range: Position.T -> Position.T -> T list -> text * Position.range
val explode: text * Position.T -> T list
- val scan_new_ident: T list -> T list * T list
val scan_ident: T list -> T list * T list
val is_identifier: string -> bool
end;
@@ -220,36 +219,46 @@
val digit = Symbol.is_ascii_digit;
fun underscore s = s = "_";
fun prime s = s = "'";
-fun script s = s = "\\<^sub>" orelse s = "\\<^isub>";
+fun subscript s = s = "\\<^sub>" orelse s = "\\<^isub>";
+fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>";
fun special_letter s = Symbol.is_letter_symbol s andalso not (script s);
val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single;
val scan_digit = Scan.one (digit o symbol) >> single;
val scan_prime = Scan.one (prime o symbol) >> single;
+val scan_extended =
+ Scan.one ((latin orf digit orf prime orf underscore orf special_letter) o symbol) >> single;
-val scan_script =
- Scan.one (script o symbol) -- Scan.one ((latin orf digit orf prime orf special_letter) o symbol)
+val scan_subscript =
+ Scan.one (subscript o symbol) --
+ Scan.one ((latin orf digit orf prime orf special_letter) o symbol)
>> (fn (x, y) => [x, y]);
val scan_ident_part1 =
- Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_script) >> flat) ||
+ Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_subscript) >> flat) ||
Scan.one (special_letter o symbol) :::
- (Scan.repeat (scan_digit || scan_prime || scan_script) >> flat);
+ (Scan.repeat (scan_digit || scan_prime || scan_subscript) >> flat);
val scan_ident_part2 =
- Scan.repeat1 (scan_plain || scan_script) >> flat ||
+ Scan.repeat1 (scan_plain || scan_subscript) >> flat ||
scan_ident_part1;
in
-val scan_new_ident =
+val scan_ident0 =
+ Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
+
+val scan_ident1 =
+ Scan.one ((latin orf special_letter) o symbol) :::
+ (Scan.repeat (scan_extended || Scan.one (subscript o symbol) ::: scan_extended) >> flat);
+
+val scan_ident2 =
scan_ident_part1 @@@
(Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat);
end;
-val scan_ident =
- Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
+val scan_ident = scan_ident0;
fun is_identifier s =
Symbol.is_ascii_identifier s orelse
--- a/src/Pure/library.scala Wed Dec 12 15:38:47 2012 +0100
+++ b/src/Pure/library.scala Wed Dec 12 19:03:49 2012 +0100
@@ -178,8 +178,16 @@
if (10 <= i && i <= 1000) i else 100
case _ => 100
}
+
def print(i: Int): String = i.toString + "%"
+ def set_item(i: Int) {
+ peer.getEditor match {
+ case null =>
+ case editor => editor.setItem(print(i))
+ }
+ }
+
makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x))
reactions += {
case SelectionChanged(_) => apply_factor(parse(selection.item))
--- a/src/Tools/Graphview/src/graph_panel.scala Wed Dec 12 15:38:47 2012 +0100
+++ b/src/Tools/Graphview/src/graph_panel.scala Wed Dec 12 19:03:49 2012 +0100
@@ -51,8 +51,10 @@
def refresh()
{
- paint_panel.set_preferred_size()
- paint_panel.repaint()
+ if (paint_panel != null) {
+ paint_panel.set_preferred_size()
+ paint_panel.repaint()
+ }
}
def fit_to_window() = {
@@ -60,9 +62,13 @@
refresh()
}
+ val zoom_box: Library.Zoom_Box =
+ new Library.Zoom_Box(percent => rescale(0.01 * percent))
+
def rescale(s: Double)
{
Transform.scale = s
+ if (zoom_box != null) zoom_box.set_item((Transform.scale_discrete * 100).round.toInt)
refresh()
}
@@ -109,7 +115,7 @@
visualizer.model.Mutators.events += { case _ => repaint() }
apply_layout()
- fit_to_window()
+ rescale(1.0)
private object Transform
{
@@ -120,7 +126,6 @@
def scale_=(s: Double)
{
_scale = (s min 10) max 0.1
- paint_panel.set_preferred_size()
}
def scale_discrete: Double =
(_scale * visualizer.font_size).round.toDouble / visualizer.font_size
@@ -135,13 +140,13 @@
def fit_to_window() {
if (visualizer.model.visible_nodes().isEmpty)
- scale = 1
+ rescale(1.0)
else {
val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds()
val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
val (sx, sy) = (1.0 * size.width / dx, 1.0 * size.height / dy)
- scale = sx min sy
+ rescale(sx min sy)
}
}
@@ -164,8 +169,8 @@
def typed(c: Char, m: Modifiers) =
(c, m) match {
- case ('+', _) => Transform.scale *= 5.0/4
- case ('-', _) => Transform.scale *= 4.0/5
+ case ('+', _) => rescale(Transform.scale * 5.0/4)
+ case ('-', _) => rescale(Transform.scale * 4.0/5)
case ('0', _) => Transform.fit_to_window()
case ('1', _) => visualizer.Coordinates.update_layout()
case ('2', _) => Transform.fit_to_window()
@@ -275,7 +280,7 @@
def wheel(rotation: Int, at: Point) {
val at2 = Transform.pane_to_graph_coordinates(at)
// > 0 -> up
- Transform.scale *= (if (rotation > 0) 4.0/5 else 5.0/4)
+ rescale(Transform.scale * (if (rotation > 0) 4.0/5 else 5.0/4))
// move mouseposition to center
Transform().transform(at2, at2)
--- a/src/Tools/Graphview/src/main_panel.scala Wed Dec 12 15:38:47 2012 +0100
+++ b/src/Tools/Graphview/src/main_panel.scala Wed Dec 12 19:03:49 2012 +0100
@@ -71,7 +71,7 @@
}
}
contents += Swing.RigidBox(new Dimension(10, 0))
- contents += new Library.Zoom_Box(percent => graph_panel.rescale(0.01 * percent))
+ contents += graph_panel.zoom_box
contents += Swing.RigidBox(new Dimension(10, 0))
contents += new Button{
--- a/src/Tools/jEdit/src/jEdit.props Wed Dec 12 15:38:47 2012 +0100
+++ b/src/Tools/jEdit/src/jEdit.props Wed Dec 12 19:03:49 2012 +0100
@@ -205,6 +205,8 @@
line-end.shortcut=END
line-home.shortcut=HOME
lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
+plugin.MacOSXPlugin.altDispatcher=true
+plugin.MacOSXPlugin.disableOption=true
print.font=IsabelleText
restore.remote=false
restore=false