--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML Thu Nov 22 17:26:06 2012 +0100
@@ -130,7 +130,7 @@
fun output_line cert =
"To repeat this proof with a certifiate use this command:\n" ^
- Markup.markup Isabelle_Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
+ Sendback.markup ("by (sos_cert \"" ^ cert ^ "\")")
val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
--- a/src/HOL/Statespace/StateSpaceEx.thy Thu Nov 22 14:44:37 2012 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy Thu Nov 22 17:26:06 2012 +0100
@@ -235,7 +235,7 @@
ML {*
fun make_benchmark n =
- writeln (Markup.markup Isabelle_Markup.sendback
+ writeln (Sendback.markup
("statespace benchmark" ^ string_of_int n ^ " =\n" ^
(cat_lines (map (fn i => "A" ^ string_of_int i ^ "::nat") (1 upto n)))));
*}
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Thu Nov 22 17:26:06 2012 +0100
@@ -470,7 +470,7 @@
pprint_nt (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
\general enough, try this command: " @
- [Pretty.mark Isabelle_Markup.sendback (Pretty.blk (0,
+ [Pretty.mark (Sendback.make_markup ()) (Pretty.blk (0,
pstrs ("nitpick [non_std, show_all]")))] @ pstrs "."))
else
()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Nov 22 17:26:06 2012 +0100
@@ -754,8 +754,7 @@
(true, "")
end)
-fun sendback sub =
- Markup.markup Isabelle_Markup.sendback (sledgehammerN ^ " " ^ sub)
+fun sendback sub = Sendback.markup (sledgehammerN ^ " " ^ sub)
val commit_timeout = seconds 30.0
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Nov 22 17:26:06 2012 +0100
@@ -233,15 +233,14 @@
command_call (string_for_reconstructor reconstr) ss
fun try_command_line banner time command =
- banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^
- show_time time ^ "."
+ banner ^ ": " ^ Sendback.markup command ^ show_time time ^ "."
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
"" => ""
| command =>
- "\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "."
+ "\nTo minimize: " ^ Sendback.markup command ^ "."
fun split_used_facts facts =
facts |> List.partition (fn (_, (sc, _)) => sc = Chained)
@@ -1055,7 +1054,7 @@
else if preplay then
" (" ^ string_from_ext_time ext_time ^ ")"
else
- "") ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
+ "") ^ ":\n" ^ Sendback.markup isar_text
end
val isar_proof =
if debug then
--- a/src/HOL/Tools/try0.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/HOL/Tools/try0.ML Thu Nov 22 17:26:06 2012 +0100
@@ -138,7 +138,7 @@
Auto_Try => "Auto Try Methods found a proof"
| Try => "Try Methods found a proof"
| Normal => "Try this") ^ ": " ^
- Markup.markup Isabelle_Markup.sendback
+ Sendback.markup
((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
"\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
--- a/src/Pure/General/pretty.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Pure/General/pretty.ML Thu Nov 22 17:26:06 2012 +0100
@@ -40,6 +40,9 @@
val marks_str: Markup.T list * string -> T
val command: string -> T
val keyword: string -> T
+ val text: string -> T list
+ val paragraph: T list -> T
+ val para: string -> T
val markup_chunks: Markup.T -> T list -> T
val chunks: T list -> T
val chunks2: T list -> T
@@ -156,6 +159,10 @@
fun command name = mark_str (Isabelle_Markup.keyword1, name);
fun keyword name = mark_str (Isabelle_Markup.keyword2, name);
+val text = breaks o map str o Symbol.explode_words;
+val paragraph = markup Isabelle_Markup.paragraph;
+val para = paragraph o text;
+
fun markup_chunks m prts = markup m (fbreaks prts);
val chunks = markup_chunks Markup.empty;
fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
--- a/src/Pure/General/symbol.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Pure/General/symbol.ML Thu Nov 22 17:26:06 2012 +0100
@@ -56,6 +56,8 @@
val scan_id: string list -> string * string list
val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source
val explode: string -> symbol list
+ val split_words: symbol list -> string list
+ val explode_words: string -> string list
val esc: symbol -> string
val escape: string -> string
val strip_blanks: string -> string
@@ -170,7 +172,7 @@
val raw0 = enclose "\\<^raw:" ">";
val raw1 = raw0 o implode;
val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
-
+
fun encode cs = enc (take_prefix raw_chr cs)
and enc ([], []) = []
| enc (cs, []) = [raw1 cs]
@@ -399,13 +401,13 @@
(* scanning through symbols *)
-fun scanner msg scan chs =
+fun scanner msg scan syms =
let
- fun message (cs, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 cs))
- | message (cs, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 cs));
- val fin_scan = Scan.error (Scan.finite stopper (!! message scan));
+ fun message (ss, NONE) = (fn () => msg ^ ": " ^ quote (beginning 10 ss))
+ | message (ss, SOME msg') = (fn () => msg ^ ", " ^ msg' () ^ ": " ^ quote (beginning 10 ss));
+ val finite_scan = Scan.error (Scan.finite stopper (!! message scan));
in
- (case fin_scan chs of
+ (case finite_scan syms of
(result, []) => result
| (_, rest) => error (message (rest, NONE) ()))
end;
@@ -470,6 +472,17 @@
end;
+(* space-separated words *)
+
+val scan_word =
+ Scan.many1 is_ascii_blank >> K NONE ||
+ Scan.many1 (fn s => not (is_ascii_blank s) andalso not_eof s) >> (SOME o implode);
+
+val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I);
+
+val explode_words = split_words o sym_explode;
+
+
(* escape *)
val esc = fn s =>
--- a/src/Pure/PIDE/command.scala Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Pure/PIDE/command.scala Thu Nov 22 17:26:06 2012 +0100
@@ -66,14 +66,16 @@
case XML.Elem(Markup(name, atts), body) =>
atts match {
case Isabelle_Markup.Serial(i) =>
- val st0 =
- copy(results =
- results + (i -> XML.Elem(Markup(Isabelle_Markup.message(name), atts), body)))
+ val props = Position.purge(atts)
+ val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
+ val message2 = XML.Elem(Markup(name, props), body)
+
+ val st0 = copy(results = results + (i -> message1))
val st1 =
if (Protocol.is_tracing(message)) st0
else
(st0 /: Protocol.message_positions(command, message))(
- (st, range) => st.add_markup(Text.Info(range, message)))
+ (st, range) => st.add_markup(Text.Info(range, message2)))
st1
case _ => System.err.println("Ignored message without serial number: " + message); this
--- a/src/Pure/PIDE/isabelle_markup.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.ML Thu Nov 22 17:26:06 2012 +0100
@@ -67,6 +67,7 @@
val ML_antiquotationN: string
val document_antiquotationN: string
val document_antiquotation_optionN: string
+ val paragraphN: string val paragraph: Markup.T
val keywordN: string val keyword: Markup.T
val operatorN: string val operator: Markup.T
val commandN: string val command: Markup.T
@@ -239,6 +240,11 @@
val document_antiquotation_optionN = "document_antiquotation_option";
+(* text structure *)
+
+val (paragraphN, paragraph) = markup_elem "paragraph";
+
+
(* outer syntax *)
val (keywordN, keyword) = markup_elem "keyword";
--- a/src/Pure/PIDE/isabelle_markup.scala Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Pure/PIDE/isabelle_markup.scala Thu Nov 22 17:26:06 2012 +0100
@@ -126,6 +126,11 @@
val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
+ /* text structure */
+
+ val PARAGRAPH = "paragraph"
+
+
/* ML syntax */
val ML_KEYWORD = "ML_keyword"
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/sendback.ML Thu Nov 22 17:26:06 2012 +0100
@@ -0,0 +1,31 @@
+(* Title: Pure/PIDE/sendback.ML
+ Author: Makarius
+
+Clickable "sendback" areas within the source text (see also
+Tools/jEdit/src/sendback.scala).
+*)
+
+signature SENDBACK =
+sig
+ val make_markup: unit -> Markup.T
+ val markup: string -> string
+ val markup_implicit: string -> string
+end;
+
+structure Sendback: SENDBACK =
+struct
+
+fun make_markup () =
+ let
+ val props =
+ (case Position.get_id (Position.thread_data ()) of
+ SOME id => [(Isabelle_Markup.idN, id)]
+ | NONE => []);
+ in Markup.properties props Isabelle_Markup.sendback end;
+
+fun markup s = Markup.markup (make_markup ()) s;
+
+val markup_implicit = Markup.markup Isabelle_Markup.sendback;
+
+end;
+
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Nov 22 17:26:06 2012 +0100
@@ -8,7 +8,6 @@
signature PROOF_GENERAL =
sig
val test_markupN: string
- val sendback: string -> Pretty.T list -> unit
val init: bool -> unit
structure ThyLoad: sig val add_path: string -> unit end
end;
@@ -113,9 +112,6 @@
fun tell_file_retracted path =
emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
-fun sendback heading prts =
- Pretty.writeln (Pretty.big_list heading [Pretty.markup Isabelle_Markup.sendback prts]);
-
(* theory loader actions *)
--- a/src/Pure/ROOT Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Pure/ROOT Thu Nov 22 17:26:06 2012 +0100
@@ -147,6 +147,7 @@
"PIDE/isabelle_markup.ML"
"PIDE/markup.ML"
"PIDE/protocol.ML"
+ "PIDE/sendback.ML"
"PIDE/xml.ML"
"PIDE/yxml.ML"
"Proof/extraction.ML"
--- a/src/Pure/ROOT.ML Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Pure/ROOT.ML Thu Nov 22 17:26:06 2012 +0100
@@ -64,6 +64,7 @@
use "PIDE/xml.ML";
use "PIDE/yxml.ML";
+use "PIDE/sendback.ML";
use "General/graph.ML";
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Thu Nov 22 17:26:06 2012 +0100
@@ -245,24 +245,12 @@
}
- def sendback(range: Text.Range): Option[Text.Info[Document.Exec_ID]] =
- {
- val results =
- snapshot.cumulate_markup[(Option[Document.Exec_ID], Option[Text.Range])](range,
- (None, None), Some(messages_include + Isabelle_Markup.SENDBACK),
- {
- case ((_, info), Text.Info(_, XML.Elem(Markup(name, Position.Id(id)), _)))
- if messages_include(name) => (Some(id), info)
-
- case ((id, _), Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) =>
- (id, Some(snapshot.convert(info_range)))
- })
-
- (for (Text.Info(_, (Some(id), Some(r))) <- results) yield Text.Info(r, id)) match {
- case res #:: _ => Some(res)
- case _ => None
- }
- }
+ def sendback(range: Text.Range): Option[Text.Info[Option[Document.Exec_ID]]] =
+ snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)),
+ {
+ case Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, props), _)) =>
+ Text.Info(snapshot.convert(info_range), Position.Id.unapply(props))
+ }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
def tooltip_message(range: Text.Range): XML.Body =
--- a/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Thu Nov 22 17:26:06 2012 +0100
@@ -77,33 +77,35 @@
getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
- val font_metrics = getPainter.getFontMetrics(font)
- val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
-
- val base_snapshot = current_base_snapshot
- val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
+ if (getWidth > 0) {
+ val font_metrics = getPainter.getFontMetrics(font)
+ val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
- future_rendering.map(_.cancel(true))
- future_rendering = Some(default_thread_pool.submit(() =>
- {
- val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
- Simple_Thread.interrupted_exception()
+ val base_snapshot = current_base_snapshot
+ val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
+
+ future_rendering.map(_.cancel(true))
+ future_rendering = Some(default_thread_pool.submit(() =>
+ {
+ val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
+ Simple_Thread.interrupted_exception()
- Swing_Thread.later {
- current_rendering = rendering
+ Swing_Thread.later {
+ current_rendering = rendering
- try {
- getBuffer.beginCompoundEdit
- getBuffer.setReadOnly(false)
- setText(text)
- setCaretPosition(0)
- getBuffer.setReadOnly(true)
+ try {
+ getBuffer.beginCompoundEdit
+ getBuffer.setReadOnly(false)
+ setText(text)
+ setCaretPosition(0)
+ getBuffer.setReadOnly(true)
+ }
+ finally {
+ getBuffer.endCompoundEdit
+ }
}
- finally {
- getBuffer.endCompoundEdit
- }
- }
- }))
+ }))
+ }
}
def resize(font_family: String, font_size: Int)
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Thu Nov 22 17:26:06 2012 +0100
@@ -9,7 +9,7 @@
import isabelle._
-import java.awt.{Toolkit, Color, Point, BorderLayout, Window}
+import java.awt.{Toolkit, Color, Point, BorderLayout, Window, Dimension}
import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
import javax.swing.border.LineBorder
@@ -73,7 +73,7 @@
pretty_text_area.update(rendering.snapshot, body)
pretty_text_area.registerKeyboardAction(action_listener, "close_all",
- KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
+ KeyStroke.getKeyStroke(KeyEvent.VK_ESCAPE, 0), JComponent.WHEN_FOCUSED)
window.add(pretty_text_area)
@@ -107,14 +107,15 @@
{
val font_metrics = pretty_text_area.getPainter.getFontMetrics
val margin = Isabelle.options.int("jedit_tooltip_margin") // FIXME via rendering?!
- val lines = // FIXME avoid redundant formatting
+ val lines =
XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
val screen = Toolkit.getDefaultToolkit.getScreenSize
- val w = (font_metrics.charWidth(Pretty.spc) * margin) min (screen.width / 2)
- val h = (font_metrics.getHeight * (lines + 2) + 25) min (screen.height / 2)
- window.setSize(w, h)
+ val w = (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen.width / 2)
+ val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2)
+ pretty_text_area.setPreferredSize(new Dimension(w, h))
+ window.pack
}
{
@@ -128,6 +129,6 @@
}
window.setVisible(true)
- pretty_text_area.refresh() // FIXME avoid redundant formatting
+ pretty_text_area.refresh()
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Thu Nov 22 17:26:06 2012 +0100
@@ -136,7 +136,7 @@
private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
private val sendback_area =
- new Active_Area[Document.Exec_ID]((r: Isabelle_Rendering) => r.sendback _)
+ new Active_Area[Option[Document.Exec_ID]]((r: Isabelle_Rendering) => r.sendback _)
private val active_areas =
List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
@@ -179,7 +179,7 @@
val rendering = get_rendering()
for ((area, require_control) <- active_areas)
{
- if (control == require_control)
+ if (control == require_control && !rendering.snapshot.is_outdated)
area.update_rendering(rendering, range)
else area.reset
}
--- a/src/Tools/jEdit/src/sendback.scala Thu Nov 22 14:44:37 2012 +0100
+++ b/src/Tools/jEdit/src/sendback.scala Thu Nov 22 17:26:06 2012 +0100
@@ -14,7 +14,7 @@
object Sendback
{
- def activate(view: View, text: String, exec_id: Document.Exec_ID)
+ def activate(view: View, text: String, id: Option[Document.Exec_ID])
{
Swing_Thread.require()
@@ -25,19 +25,28 @@
val buffer = model.buffer
val snapshot = model.snapshot()
- snapshot.state.execs.get(exec_id).map(_.command) match {
- case Some(command) if !snapshot.is_outdated =>
- snapshot.node.command_start(command) match {
- case Some(start) =>
- try {
- buffer.beginCompoundEdit()
- buffer.remove(start, command.proper_range.length)
- buffer.insert(start, text)
- }
- finally { buffer.endCompoundEdit() }
- case None =>
- }
- case _ =>
+ if (!snapshot.is_outdated) {
+ id match {
+ case None =>
+ doc_view.text_area.setSelectedText(text)
+ case Some(exec_id) =>
+ snapshot.state.execs.get(exec_id).map(_.command) match {
+ case Some(command) =>
+ snapshot.node.command_start(command) match {
+ case Some(start) =>
+ try {
+ buffer.beginCompoundEdit()
+ buffer.remove(start, command.proper_range.length)
+ buffer.insert(start, text)
+ }
+ finally {
+ buffer.endCompoundEdit()
+ }
+ case None =>
+ }
+ case None =>
+ }
+ }
}
}
case None =>