# HG changeset patch # User wenzelm # Date 1353601566 -3600 # Node ID d655dda100c53b8bbb0b849e000a07edb6ba09b1 # Parent 8155e280f239e51c4952b9458c4baaea478d346d# Parent 071902349e3ef631951e5185a4cb50fe9996f3b5 merged diff -r 8155e280f239 -r d655dda100c5 src/HOL/Library/Sum_of_Squares/sos_wrapper.ML --- 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 diff -r 8155e280f239 -r d655dda100c5 src/HOL/Statespace/StateSpaceEx.thy --- 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))))); *} diff -r 8155e280f239 -r d655dda100c5 src/HOL/Tools/Nitpick/nitpick.ML --- 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 () diff -r 8155e280f239 -r d655dda100c5 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- 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 diff -r 8155e280f239 -r d655dda100c5 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- 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 diff -r 8155e280f239 -r d655dda100c5 src/HOL/Tools/try0.ML --- 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" diff -r 8155e280f239 -r d655dda100c5 src/Pure/General/pretty.ML --- 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))); diff -r 8155e280f239 -r d655dda100c5 src/Pure/General/symbol.ML --- 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 => diff -r 8155e280f239 -r d655dda100c5 src/Pure/PIDE/command.scala --- 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 diff -r 8155e280f239 -r d655dda100c5 src/Pure/PIDE/isabelle_markup.ML --- 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"; diff -r 8155e280f239 -r d655dda100c5 src/Pure/PIDE/isabelle_markup.scala --- 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" diff -r 8155e280f239 -r d655dda100c5 src/Pure/PIDE/sendback.ML --- /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; + diff -r 8155e280f239 -r d655dda100c5 src/Pure/ProofGeneral/proof_general_emacs.ML --- 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 *) diff -r 8155e280f239 -r d655dda100c5 src/Pure/ROOT --- 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" diff -r 8155e280f239 -r d655dda100c5 src/Pure/ROOT.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"; diff -r 8155e280f239 -r d655dda100c5 src/Tools/jEdit/src/isabelle_rendering.scala --- 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 = diff -r 8155e280f239 -r d655dda100c5 src/Tools/jEdit/src/pretty_text_area.scala --- 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) diff -r 8155e280f239 -r d655dda100c5 src/Tools/jEdit/src/pretty_tooltip.scala --- 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() } diff -r 8155e280f239 -r d655dda100c5 src/Tools/jEdit/src/rich_text_area.scala --- 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 } diff -r 8155e280f239 -r d655dda100c5 src/Tools/jEdit/src/sendback.scala --- 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 =>