# HG changeset patch
# User wenzelm
# Date 1288887441 -3600
# Node ID 3157408633ee8749c30f4d1cc52beab0216edc6f
# Parent  852d6ed1b5c63e91291a0784c53a90e0a0604ff3# Parent  088e5adca5ad4614b7b7efcc385d919786f631a6
merged

diff -r 852d6ed1b5c6 -r 3157408633ee lib/scripts/feeder
--- 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"
diff -r 852d6ed1b5c6 -r 3157408633ee lib/scripts/feeder.pl
--- 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>) {
diff -r 852d6ed1b5c6 -r 3157408633ee src/Pure/ML-Systems/timing.ML
--- 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
diff -r 852d6ed1b5c6 -r 3157408633ee src/Pure/ML/ml_lex.ML
--- 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;
diff -r 852d6ed1b5c6 -r 3157408633ee src/Tools/jEdit/plugin/Isabelle.props
--- 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
diff -r 852d6ed1b5c6 -r 3157408633ee src/Tools/jEdit/src/jedit/document_view.scala
--- 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
+          }
         }
       }
     }
diff -r 852d6ed1b5c6 -r 3157408633ee src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- 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"
diff -r 852d6ed1b5c6 -r 3157408633ee src/Tools/jEdit/src/jedit/isabelle_options.scala
--- 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]
   }