--- a/lib/scripts/feeder Thu Nov 04 13:37:11 2010 +0100
+++ b/lib/scripts/feeder Thu Nov 04 17:17:21 2010 +0100
@@ -16,7 +16,7 @@
echo "Usage: $PRG [OPTIONS]"
echo
echo " Options are:"
- echo " -h TEXT head text"
+ echo " -h TEXT head text (encoded as utf8)"
echo " -p emit my pid"
echo " -q do not pipe stdin"
echo " -t TEXT tail text"
--- a/lib/scripts/feeder.pl Thu Nov 04 13:37:11 2010 +0100
+++ b/lib/scripts/feeder.pl Thu Nov 04 17:17:21 2010 +0100
@@ -24,7 +24,11 @@
$emitpid && (print $$, "\n");
-$head && (print "$head", "\n");
+if ($head) {
+ utf8::encode($head);
+ $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g;
+ print $head, "\n";
+}
if (!$quit) {
while (<STDIN>) {
--- a/src/Pure/ML-Systems/timing.ML Thu Nov 04 13:37:11 2010 +0100
+++ b/src/Pure/ML-Systems/timing.ML Thu Nov 04 17:17:21 2010 +0100
@@ -1,10 +1,10 @@
(* Title: Pure/ML-Systems/timing.ML
Author: Makarius
-Basic support for timing.
+Basic support for time measurement.
*)
-fun seconds s = Time.fromNanoseconds (Real.ceil (s * 1E9));
+val seconds = Time.fromReal;
fun start_timing () =
let
--- a/src/Pure/ML/ml_lex.ML Thu Nov 04 13:37:11 2010 +0100
+++ b/src/Pure/ML/ml_lex.ML Thu Nov 04 17:17:21 2010 +0100
@@ -70,17 +70,18 @@
fun content_of (Token (_, (_, x))) = x;
fun token_leq (tok, tok') = content_of tok <= content_of tok';
+fun warn tok =
+ (case tok of
+ Token (_, (Keyword, ":>")) =>
+ warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
+ \prefer non-opaque matching (:) possibly with abstype" ^
+ Position.str_of (pos_of tok))
+ | _ => ());
+
fun check_content_of tok =
(case kind_of tok of
Error msg => error msg
- | _ =>
- (case tok of
- Token (_, (Keyword, ":>")) =>
- warning ("Opaque signature matching (:>) fails to work with ML pretty printing --\n\
- \prefer non-opaque matching (:) possibly with abstype" ^
- Position.str_of (pos_of tok))
- | _ => ();
- content_of tok));
+ | _ => content_of tok);
val flatten = implode o map (Symbol.escape o check_content_of);
@@ -288,7 +289,7 @@
|> Source.exhaust
|> tap (List.app (Antiquote.report report_token))
|> tap Antiquote.check_nesting
- |> tap (List.app (fn Antiquote.Text tok => ignore (check_content_of tok) | _ => ())))
+ |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
handle ERROR msg =>
cat_error msg ("The error(s) above occurred in ML source" ^ Position.str_of pos);
in input @ termination end;
--- a/src/Tools/jEdit/plugin/Isabelle.props Thu Nov 04 13:37:11 2010 +0100
+++ b/src/Tools/jEdit/plugin/Isabelle.props Thu Nov 04 17:17:21 2010 +0100
@@ -29,6 +29,8 @@
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=40
options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
options.isabelle.tooltip-dismiss-delay=8000
options.isabelle.startup-timeout=10000
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Nov 04 13:37:11 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Nov 04 17:17:21 2010 +0100
@@ -165,6 +165,8 @@
/* CONTROL-mouse management */
+ private var control: Boolean = false
+
private def exit_control()
{
exit_popup()
@@ -184,7 +186,7 @@
private val mouse_motion_listener = new MouseMotionAdapter {
override def mouseMoved(e: MouseEvent) {
- val control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+ control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
val x = e.getX()
val y = e.getY()
@@ -288,10 +290,20 @@
Isabelle.swing_buffer_lock(model.buffer) {
val snapshot = model.snapshot()
val offset = text_area.xyToOffset(x, y)
- snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
- {
- case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
- case _ => null
+ if (control) {
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+ case _ => null
+ }
+ }
+ else {
+ // FIXME snapshot.cumulate
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+ case _ => null
+ }
}
}
}
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Thu Nov 04 13:37:11 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Thu Nov 04 17:17:21 2010 +0100
@@ -84,10 +84,11 @@
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
}
- val popup: Markup_Tree.Select[XML.Tree] =
+ val popup: Markup_Tree.Select[String] =
{
case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
- if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => msg
+ if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
+ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
}
val gutter_message: Markup_Tree.Select[Icon] =
@@ -109,7 +110,8 @@
val tooltip: Markup_Tree.Select[String] =
{
case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
- Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), margin = 40)
+ Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
+ margin = Isabelle.Int_Property("tooltip-margin"))
case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Thu Nov 04 13:37:11 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Thu Nov 04 17:17:21 2010 +0100
@@ -20,6 +20,7 @@
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()
override def _init()
@@ -35,6 +36,9 @@
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.Int_Property("tooltip-dismiss-delay", 8000))
addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
}
@@ -51,6 +55,9 @@
Isabelle.Int_Property("tooltip-font-size") =
tooltip_font_size.getValue().asInstanceOf[Int]
+ Isabelle.Int_Property("tooltip-margin") =
+ tooltip_margin.getValue().asInstanceOf[Int]
+
Isabelle.Int_Property("tooltip-dismiss-delay") =
tooltip_dismiss_delay.getValue().asInstanceOf[Int]
}