--- a/NEWS Thu Feb 20 16:56:33 2014 +0100
+++ b/NEWS Thu Feb 20 21:45:08 2014 +0100
@@ -340,6 +340,15 @@
intervals.
+*** Scala ***
+
+* The signature and semantics of Document.Snapshot.cumulate_markup /
+select_markup have been clarified. Markup is now traversed in the
+order of reports given by the prover: later markup is usually more
+specific and may override results accumulated so far. The elements
+guard is mandatory and checked precisely. Subtle INCOMPATIBILITY.
+
+
*** ML ***
* Proper context discipline for read_instantiate and instantiate_tac:
--- a/src/HOL/HOL.thy Thu Feb 20 16:56:33 2014 +0100
+++ b/src/HOL/HOL.thy Thu Feb 20 21:45:08 2014 +0100
@@ -24,7 +24,6 @@
ML_file "~~/src/Provers/classical.ML"
ML_file "~~/src/Provers/blast.ML"
ML_file "~~/src/Provers/clasimp.ML"
-ML_file "~~/src/Tools/coherent.ML"
ML_file "~~/src/Tools/eqsubst.ML"
ML_file "~~/src/Provers/quantifier1.ML"
ML_file "~~/src/Tools/atomize_elim.ML"
@@ -1561,20 +1560,18 @@
subsubsection {* Coherent logic *}
+ML_file "~~/src/Tools/coherent.ML"
ML {*
structure Coherent = Coherent
(
- val atomize_elimL = @{thm atomize_elimL}
- val atomize_exL = @{thm atomize_exL}
- val atomize_conjL = @{thm atomize_conjL}
- val atomize_disjL = @{thm atomize_disjL}
- val operator_names =
- [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}]
+ val atomize_elimL = @{thm atomize_elimL};
+ val atomize_exL = @{thm atomize_exL};
+ val atomize_conjL = @{thm atomize_conjL};
+ val atomize_disjL = @{thm atomize_disjL};
+ val operator_names = [@{const_name HOL.disj}, @{const_name HOL.conj}, @{const_name Ex}];
);
*}
-setup Coherent.setup
-
subsubsection {* Reorienting equalities *}
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 20 21:45:08 2014 +0100
@@ -531,7 +531,7 @@
|> AList.group (op =)
|> map (fn (a, xs) => string_for_annotation a ^ ": " ^
string_for_vars ", " (sort int_ord xs))
- |> space_implode "\n"))
+ |> cat_lines))
(* The ML solver timeout should correspond more or less to the overhead of invoking an external
prover. *)
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Thu Feb 20 21:45:08 2014 +0100
@@ -209,7 +209,7 @@
(if null iters then [] else ["iter: " ^ commas (map implode iters)]) @
miscs of
[] => "empty"
- | lines => space_implode "\n" lines
+ | lines => cat_lines lines
end
fun scopes_equivalent (s1 : scope, s2 : scope) =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Thu Feb 20 21:45:08 2014 +0100
@@ -25,7 +25,7 @@
fun print_intross options thy msg intross =
if show_intermediate_results options then
tracing (msg ^
- (space_implode "\n" (map
+ (cat_lines (map
(fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^
commas (map (Display.string_of_thm_global thy) intros)) intross)))
else ()
@@ -34,8 +34,8 @@
if show_intermediate_results options then
map (fn (c, thms) =>
"Constant " ^ c ^ " has specification:\n" ^
- (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
- |> space_implode "\n" |> tracing
+ (cat_lines (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
+ |> cat_lines |> tracing
else ()
fun overload_const thy s = the_default s (Option.map fst (Axclass.inst_of_param thy s))
--- a/src/Pure/GUI/swing_thread.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/GUI/swing_thread.scala Thu Feb 20 21:45:08 2014 +0100
@@ -7,6 +7,7 @@
package isabelle
+
import javax.swing.{SwingUtilities, Timer}
import java.awt.event.{ActionListener, ActionEvent}
--- a/src/Pure/General/antiquote.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/General/antiquote.ML Thu Feb 20 21:45:08 2014 +0100
@@ -9,7 +9,8 @@
type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
datatype 'a antiquote = Text of 'a | Antiq of antiq
val is_text: 'a antiquote -> bool
- val reports_of: ('a -> Position.report_text list) ->
+ val antiq_reports: antiq -> Position.report list
+ val antiquote_reports: ('a -> Position.report_text list) ->
'a antiquote list -> Position.report_text list
val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
val scan_antiquote: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list
@@ -30,11 +31,11 @@
(* reports *)
-fun reports_of_antiq ((_, {start, stop, range = (pos, _)}): antiq) =
- map (rpair "") [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
+fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) =
+ [(start, Markup.antiquote), (stop, Markup.antiquote), (pos, Markup.antiquoted)];
-fun reports_of text =
- maps (fn Text x => text x | Antiq antiq => reports_of_antiq antiq);
+fun antiquote_reports text =
+ maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq));
(* scan *)
@@ -75,7 +76,7 @@
fun read (syms, pos) =
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
- SOME xs => (Position.reports_text (reports_of (K []) xs); xs)
+ SOME xs => (Position.reports_text (antiquote_reports (K []) xs); xs)
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
end;
--- a/src/Pure/General/bytes.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/General/bytes.scala Thu Feb 20 21:45:08 2014 +0100
@@ -29,7 +29,7 @@
if (length == 0) empty
else {
val b = new Array[Byte](length)
- java.lang.System.arraycopy(a, offset, b, 0, length)
+ System.arraycopy(a, offset, b, 0, length)
new Bytes(b, 0, b.length)
}
@@ -101,8 +101,8 @@
else if (isEmpty) other
else {
val new_bytes = new Array[Byte](length + other.length)
- java.lang.System.arraycopy(bytes, offset, new_bytes, 0, length)
- java.lang.System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
+ System.arraycopy(bytes, offset, new_bytes, 0, length)
+ System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
new Bytes(new_bytes, 0, new_bytes.length)
}
--- a/src/Pure/General/linear_set.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/General/linear_set.scala Thu Feb 20 21:45:08 2014 +0100
@@ -8,6 +8,7 @@
package isabelle
+
import scala.collection.SetLike
import scala.collection.generic.{ImmutableSetFactory, CanBuildFrom,
GenericSetTemplate, GenericCompanion}
--- a/src/Pure/General/multi_map.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/General/multi_map.scala Thu Feb 20 21:45:08 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
--- a/src/Pure/General/position.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/General/position.ML Thu Feb 20 21:45:08 2014 +0100
@@ -187,15 +187,15 @@
fun here pos =
let
val props = properties_of pos;
- val s =
+ val (s1, s2) =
(case (line_of pos, file_of pos) of
- (SOME i, NONE) => "(line " ^ Markup.print_int i ^ ")"
- | (SOME i, SOME name) => "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")"
- | (NONE, SOME name) => "(file " ^ quote name ^ ")"
- | _ => if is_reported pos then "\\<here>" else "");
+ (SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
+ | (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
+ | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
+ | _ => if is_reported pos then ("", "\\<here>") else ("", ""));
in
if null props then ""
- else (if s = "" then "" else " ") ^ Markup.markup (Markup.properties props Markup.position) s
+ else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
end;
val here_list = space_implode " " o map here;
--- a/src/Pure/General/symbol.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/General/symbol.scala Thu Feb 20 21:45:08 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.collection.mutable
import scala.util.matching.Regex
import scala.annotation.tailrec
--- a/src/Pure/General/timing.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/General/timing.scala Thu Feb 20 21:45:08 2014 +0100
@@ -14,13 +14,13 @@
def timeit[A](message: String, enabled: Boolean = true)(e: => A) =
if (enabled) {
- val start = java.lang.System.currentTimeMillis()
+ val start = System.currentTimeMillis()
val result = Exn.capture(e)
- val stop = java.lang.System.currentTimeMillis()
+ val stop = System.currentTimeMillis()
val timing = Time.ms(stop - start)
if (timing.is_relevant)
- java.lang.System.err.println(
+ System.err.println(
(if (message == null || message.isEmpty) "" else message + ": ") +
timing.message + " elapsed time")
--- a/src/Pure/Isar/completion.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Isar/completion.scala Thu Feb 20 21:45:08 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.collection.immutable.SortedMap
import scala.util.parsing.combinator.RegexParsers
import scala.math.Ordering
@@ -13,6 +14,19 @@
object Completion
{
+ /* context */
+
+ object Context
+ {
+ val default = Context("", true)
+ }
+
+ sealed case class Context(language: String, symbols: Boolean)
+ {
+ def is_outer: Boolean = language == ""
+ }
+
+
/* result */
sealed case class Item(
@@ -42,7 +56,7 @@
def load(): History =
{
def ignore_error(msg: String): Unit =
- java.lang.System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY +
+ System.err.println("### Ignoring bad content of file " + COMPLETION_HISTORY +
(if (msg == "") "" else "\n" + msg))
val content =
@@ -113,20 +127,22 @@
}
- /** word completion **/
+ /** word parsers **/
- private val word_regex = "[a-zA-Z0-9_']+".r
- private def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
-
- private object Parse extends RegexParsers
+ private object Word_Parsers extends RegexParsers
{
override val whiteSpace = "".r
- def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
- def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
- def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
- def word: Parser[String] = word_regex
- def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
+ private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
+ private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
+ private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
+
+ private val word_regex = "[a-zA-Z0-9_']+".r
+ private def word: Parser[String] = word_regex
+ private def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
+
+ def is_word(s: CharSequence): Boolean =
+ word_regex.pattern.matcher(s).matches
def read(explicit: Boolean, in: CharSequence): Option[String] =
{
@@ -141,6 +157,7 @@
}
final class Completion private(
+ keywords: Set[String] = Set.empty,
words_lex: Scan.Lexicon = Scan.Lexicon.empty,
words_map: Multi_Map[String, String] = Multi_Map.empty,
abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
@@ -150,6 +167,7 @@
def + (keyword: String, replace: String): Completion =
new Completion(
+ keywords + keyword,
words_lex + keyword,
words_map + (keyword -> replace),
abbrevs_lex,
@@ -160,15 +178,16 @@
private def add_symbols(): Completion =
{
val words =
- (for ((x, _) <- Symbol.names) yield (x, x)).toList :::
- (for ((x, y) <- Symbol.names) yield ("\\" + y, x)).toList :::
- (for ((x, y) <- Symbol.abbrevs.iterator if Completion.is_word(y)) yield (y, x)).toList
+ (for ((x, _) <- Symbol.names.toList) yield (x, x)) :::
+ (for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) :::
+ (for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x))
val abbrs =
- (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.is_word(y))
- yield (y.reverse.toString, (y, x))).toList
+ (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y))
+ yield (y.reverse, (y, x))).toList
new Completion(
+ keywords,
words_lex ++ words.map(_._1),
words_map ++ words,
abbrevs_lex ++ abbrs.map(_._1),
@@ -182,34 +201,45 @@
history: Completion.History,
decode: Boolean,
explicit: Boolean,
- line: CharSequence): Option[Completion.Result] =
+ text: CharSequence,
+ context: Completion.Context): Option[Completion.Result] =
{
- val raw_result =
- Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(line)) match {
- case Scan.Parsers.Success(reverse_a, _) =>
- val abbrevs = abbrevs_map.get_list(reverse_a)
- abbrevs match {
- case Nil => None
- case (a, _) :: _ => Some((a, abbrevs.map(_._2)))
- }
- case _ =>
- Completion.Parse.read(explicit, line) match {
- case Some(word) =>
- words_lex.completions(word).map(words_map.get_list(_)).flatten match {
- case Nil => None
- case cs => Some(word, cs)
- }
- case None => None
- }
+ val abbrevs_result =
+ if (context.symbols)
+ Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match {
+ case Scan.Parsers.Success(reverse_a, _) =>
+ val abbrevs = abbrevs_map.get_list(reverse_a)
+ abbrevs match {
+ case Nil => None
+ case (a, _) :: _ => Some((a, abbrevs.map(_._2)))
+ }
+ case _ => None
+ }
+ else None
+
+ val words_result =
+ abbrevs_result orElse {
+ Completion.Word_Parsers.read(explicit, text) match {
+ case Some(word) =>
+ val completions =
+ for {
+ s <- words_lex.completions(word)
+ if (if (keywords(s)) context.is_outer else context.symbols)
+ r <- words_map.get_list(s)
+ } yield r
+ if (completions.isEmpty) None
+ else Some(word, completions)
+ case None => None
+ }
}
- raw_result match {
+
+ words_result match {
case Some((word, cs)) =>
- val ds =
- (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
+ val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
if (ds.isEmpty) None
else {
val immediate =
- !Completion.is_word(word) &&
+ !Completion.Word_Parsers.is_word(word) &&
Character.codePointCount(word, 0, word.length) > 1
val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate))
Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering)))
--- a/src/Pure/Isar/outer_syntax.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Thu Feb 20 21:45:08 2014 +0100
@@ -43,6 +43,7 @@
keywords: Map[String, (String, List[String])] = Map.empty,
lexicon: Scan.Lexicon = Scan.Lexicon.empty,
val completion: Completion = Completion.empty,
+ val completion_context: Completion.Context = Completion.Context.default,
val has_tokens: Boolean = true)
{
override def toString: String =
@@ -72,7 +73,7 @@
val completion1 =
if (Keyword.control(kind._1) || replace == Some("")) completion
else completion + (name, replace getOrElse name)
- new Outer_Syntax(keywords1, lexicon1, completion1, true)
+ new Outer_Syntax(keywords1, lexicon1, completion1, completion_context, true)
}
def + (name: String, kind: (String, List[String])): Outer_Syntax =
@@ -120,15 +121,10 @@
/* token language */
- def no_tokens: Outer_Syntax =
- {
- require(keywords.isEmpty && lexicon.isEmpty)
- new Outer_Syntax(completion = completion, has_tokens = false)
- }
-
def scan(input: Reader[Char]): List[Token] =
{
- Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match {
+ Token.Parsers.parseAll(
+ Token.Parsers.rep(Token.Parsers.token(lexicon, is_command)), input) match {
case Token.Parsers.Success(tokens, _) => tokens
case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
}
@@ -151,4 +147,19 @@
}
(toks.toList, ctxt)
}
+
+
+ /* language context */
+
+ def set_completion_context(context: Completion.Context): Outer_Syntax =
+ new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
+
+ def no_tokens: Outer_Syntax =
+ {
+ require(keywords.isEmpty && lexicon.isEmpty)
+ new Outer_Syntax(
+ completion = completion,
+ completion_context = completion_context,
+ has_tokens = false)
+ }
}
--- a/src/Pure/Isar/parse.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Isar/parse.scala Thu Feb 20 21:45:08 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import scala.util.parsing.combinator.Parsers
import scala.annotation.tailrec
--- a/src/Pure/ML/ml_antiquote.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/ML/ml_antiquote.ML Thu Feb 20 21:45:08 2014 +0100
@@ -68,15 +68,17 @@
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
value (Binding.name "theory")
- (Args.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) =>
- (Position.report pos (Theory.get_markup (Context.get_theory thy name));
- "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+ (Context_Position.report ctxt pos
+ (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+ "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
|| Scan.succeed "Proof_Context.theory_of ML_context") #>
value (Binding.name "theory_context")
- (Args.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) =>
- (Position.report pos (Theory.get_markup (Context.get_theory thy name));
- "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
+ (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) =>
+ (Context_Position.report ctxt pos
+ (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name));
+ "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
ML_Syntax.print_string name))) #>
inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
--- a/src/Pure/ML/ml_lex.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML Thu Feb 20 21:45:08 2014 +0100
@@ -314,7 +314,7 @@
|> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
(SOME (false, fn msg => recover msg >> map Antiquote.Text))
|> Source.exhaust
- |> tap (Position.reports_text o Antiquote.reports_of (single o report_of_token))
+ |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token))
|> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
in input @ termination end;
--- a/src/Pure/PIDE/command.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/PIDE/command.scala Thu Feb 20 21:45:08 2014 +0100
@@ -90,18 +90,17 @@
(this /: msgs)((state, msg) =>
msg match {
case elem @ XML.Elem(markup, Nil) =>
- state.add_status(markup)
- .add_markup("", Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
+ state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem))
case _ =>
- java.lang.System.err.println("Ignored status message: " + msg)
+ System.err.println("Ignored status message: " + msg)
state
})
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
{
- def bad(): Unit = java.lang.System.err.println("Ignored report message: " + msg)
+ def bad(): Unit = System.err.println("Ignored report message: " + msg)
msg match {
case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
@@ -147,7 +146,7 @@
st
case _ =>
- java.lang.System.err.println("Ignored message without serial number: " + message)
+ System.err.println("Ignored message without serial number: " + message)
this
}
}
--- a/src/Pure/PIDE/document.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/PIDE/document.scala Thu Feb 20 21:45:08 2014 +0100
@@ -369,11 +369,11 @@
def cumulate_markup[A](
range: Text.Range,
info: A,
- elements: Option[Set[String]],
+ elements: String => Boolean,
result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]]
def select_markup[A](
range: Text.Range,
- elements: Option[Set[String]],
+ elements: String => Boolean,
result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]]
}
@@ -629,7 +629,7 @@
(thy_load_commands zip other.thy_load_commands).forall(eq_commands)
}
- def cumulate_markup[A](range: Text.Range, info: A, elements: Option[Set[String]],
+ def cumulate_markup[A](range: Text.Range, info: A, elements: String => Boolean,
result: Command.State => (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{
val former_range = revert(range)
@@ -659,7 +659,7 @@
}
}
- def select_markup[A](range: Text.Range, elements: Option[Set[String]],
+ def select_markup[A](range: Text.Range, elements: String => Boolean,
result: Command.State => Text.Markup => Option[A]): List[Text.Info[A]] =
{
def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
@@ -671,7 +671,7 @@
case some => Some(some)
}
}
- for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1))
+ for (Text.Info(r, Some(x)) <- cumulate_markup(range, None, elements, result1 _))
yield Text.Info(r, x)
}
}
--- a/src/Pure/PIDE/markup.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Thu Feb 20 21:45:08 2014 +0100
@@ -20,7 +20,8 @@
val name: string -> T -> T
val kindN: string
val instanceN: string
- val languageN: string val language: string -> T
+ val symbolsN: string
+ val languageN: string val language: string -> bool -> T
val language_sort: T
val language_type: T
val language_term: T
@@ -28,6 +29,7 @@
val language_ML: T
val language_document: T
val language_text: T
+ val language_rail: T
val bindingN: string val binding: T
val entityN: string val entity: string -> string -> T
val get_entity_kind: T -> string option
@@ -245,16 +247,19 @@
(* embedded languages *)
-val (languageN, language) = markup_string "language" nameN;
+val symbolsN = "symbols";
+val languageN = "language";
+fun language name symbols = (languageN, [(nameN, name), (symbolsN, print_bool symbols)]);
-val language_sort = language "sort";
-val language_type = language "type";
-val language_term = language "term";
-val language_prop = language "prop";
+val language_sort = language "sort" true;
+val language_type = language "type" true;
+val language_term = language "term" true;
+val language_prop = language "prop" true;
-val language_ML = language "ML";
-val language_document = language "document";
-val language_text = language "text";
+val language_ML = language "ML" false;
+val language_document = language "document" false;
+val language_text = language "text" true;
+val language_rail = language "rail" true;
(* formal entities *)
--- a/src/Pure/PIDE/markup.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Thu Feb 20 21:45:08 2014 +0100
@@ -59,7 +59,7 @@
markup match {
case Markup(ENTITY, props) =>
(props, props) match {
- case (Kind(kind), Name(name)) => Some(kind, name)
+ case (Kind(kind), Name(name)) => Some((kind, name))
case _ => None
}
case _ => None
@@ -87,8 +87,25 @@
/* embedded languages */
+ val SYMBOLS = "symbols"
+ val Symbols = new Properties.Boolean(SYMBOLS)
+
val LANGUAGE = "language"
- val Language = new Markup_String(LANGUAGE, NAME)
+ object Language
+ {
+ val ML = "ML"
+ val UNKNOWN = "unknown"
+
+ def unapply(markup: Markup): Option[(String, Boolean)] =
+ markup match {
+ case Markup(LANGUAGE, props) =>
+ (props, props) match {
+ case (Name(name), Symbols(symbols)) => Some((name, symbols))
+ case _ => None
+ }
+ case _ => None
+ }
+ }
/* external resources */
--- a/src/Pure/PIDE/markup_tree.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Thu Feb 20 21:45:08 2014 +0100
@@ -45,10 +45,10 @@
final class Elements private(private val rep: Set[String])
{
- def contains(name: String): Boolean = rep.contains(name)
+ def exists(pred: String => Boolean): Boolean = rep.exists(pred)
def + (name: String): Elements =
- if (contains(name)) this
+ if (rep(name)) this
else new Elements(rep + name)
def + (elem: XML.Elem): Elements = this + elem.markup.name
@@ -176,7 +176,7 @@
if (body.forall(e => new_range.contains(e._1)))
new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
else {
- java.lang.System.err.println("Ignored overlapping markup information: " + new_markup +
+ System.err.println("Ignored overlapping markup information: " + new_markup +
body.filter(e => !new_range.contains(e._1)).mkString("\n"))
this
}
@@ -222,22 +222,17 @@
def to_XML(text: CharSequence): XML.Body =
to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
- def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
+ def cumulate[A](root_range: Text.Range, root_info: A, elements: String => Boolean,
result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
{
- val notable: Elements => Boolean =
- result_elements match {
- case Some(res) => (elements: Elements) => res.exists(elements.contains)
- case None => (elements: Elements) => true
- }
-
def results(x: A, entry: Entry): Option[A] =
{
var y = x
var changed = false
for {
- info <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
- y1 <- result(y, Text.Info(entry.range, info))
+ elem <- entry.markup
+ if elements(elem.name)
+ y1 <- result(y, Text.Info(entry.range, elem))
} { y = y1; changed = true }
if (changed) Some(y) else None
}
@@ -250,12 +245,12 @@
case (parent, (range, entry) :: more) :: rest =>
val subrange = range.restrict(root_range)
val subtree =
- if (notable(entry.subtree_elements))
+ if (entry.subtree_elements.exists(elements))
entry.subtree.overlapping(subrange).toList
else Nil
val start = subrange.start
- (if (notable(entry.elements)) results(parent.info, entry) else None) match {
+ (if (entry.elements.exists(elements)) results(parent.info, entry) else None) match {
case Some(res) =>
val next = Text.Info(subrange, res)
val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
--- a/src/Pure/PIDE/query_operation.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/PIDE/query_operation.scala Thu Feb 20 21:45:08 2014 +0100
@@ -224,7 +224,7 @@
case _ =>
}
case bad =>
- java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
+ System.err.println("Query_Operation: ignoring bad message " + bad)
}
}
}
--- a/src/Pure/PIDE/xml.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/PIDE/xml.scala Thu Feb 20 21:45:08 2014 +0100
@@ -7,6 +7,7 @@
package isabelle
+
import java.util.WeakHashMap
import java.lang.ref.WeakReference
import javax.xml.parsers.DocumentBuilderFactory
--- a/src/Pure/Syntax/lexicon.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Syntax/lexicon.ML Thu Feb 20 21:45:08 2014 +0100
@@ -290,7 +290,9 @@
(Scan.finite Symbol_Pos.stopper (Scan.repeat scan_token)) syms of
(toks, []) => toks
| (_, ss) =>
- error (err_prefix ^ Symbol_Pos.content ss ^ Position.here (#1 (Symbol_Pos.range ss))))
+ error ("Inner lexical error" ^ Position.here (#1 (Symbol_Pos.range ss)) ^
+ Markup.markup Markup.no_report ("\nat " ^ quote (Symbol_Pos.content ss))))
+
end;
--- a/src/Pure/Syntax/parser.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Syntax/parser.ML Thu Feb 20 21:45:08 2014 +0100
@@ -704,11 +704,18 @@
val toks = if Lexicon.is_eof prev_token then indata else prev_token :: indata;
val pos = Position.here (Lexicon.pos_of_token prev_token);
in
- if null toks then error ("Inner syntax error: unexpected end of input" ^ pos)
- else error (Pretty.string_of (Pretty.block
- (Pretty.str ("Inner syntax error" ^ pos ^ " at \"") ::
- Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @
- [Pretty.str "\""])))
+ if null toks then
+ error ("Inner syntax error: unexpected end of input" ^ pos)
+ else
+ error ("Inner syntax error" ^ pos ^
+ Markup.markup Markup.no_report
+ ("\n" ^ Pretty.string_of
+ (Pretty.block [
+ Pretty.str "at", Pretty.brk 1,
+ Pretty.block
+ (Pretty.str "\"" ::
+ Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @
+ [Pretty.str "\""])])))
end
| s =>
(case indata of
--- a/src/Pure/System/command_line.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/System/command_line.scala Thu Feb 20 21:45:08 2014 +0100
@@ -30,7 +30,7 @@
catch {
case exn: Throwable =>
if (debug) exn.printStackTrace
- java.lang.System.err.println(Exn.message(exn))
+ System.err.println(Exn.message(exn))
2
}
sys.exit(rc)
--- a/src/Pure/System/event_bus.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/System/event_bus.scala Thu Feb 20 21:45:08 2014 +0100
@@ -7,6 +7,7 @@
package isabelle
+
import scala.actors.Actor, Actor._
import scala.collection.mutable.ListBuffer
--- a/src/Pure/System/isabelle_charset.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/System/isabelle_charset.scala Thu Feb 20 21:45:08 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import java.nio.Buffer
import java.nio.{ByteBuffer, CharBuffer}
import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult}
--- a/src/Pure/System/isabelle_font.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/System/isabelle_font.scala Thu Feb 20 21:45:08 2014 +0100
@@ -6,6 +6,7 @@
package isabelle
+
import java.awt.{GraphicsEnvironment, Font}
import java.io.{FileInputStream, BufferedInputStream}
import javafx.scene.text.{Font => JFX_Font}
--- a/src/Pure/System/isabelle_process.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/System/isabelle_process.scala Thu Feb 20 21:45:08 2014 +0100
@@ -7,7 +7,7 @@
package isabelle
-import java.lang.System
+
import java.util.concurrent.LinkedBlockingQueue
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
InputStream, OutputStream, BufferedOutputStream, IOException}
--- a/src/Pure/System/isabelle_system.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/System/isabelle_system.scala Thu Feb 20 21:45:08 2014 +0100
@@ -7,7 +7,7 @@
package isabelle
-import java.lang.System
+
import java.util.regex.Pattern
import java.io.{File => JFile, BufferedReader, InputStreamReader,
BufferedWriter, OutputStreamWriter}
--- a/src/Pure/System/options.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/System/options.scala Thu Feb 20 21:45:08 2014 +0100
@@ -140,13 +140,13 @@
val options = (Options.init() /: more_options)(_ + _)
if (get_option != "")
- java.lang.System.out.println(options.check_name(get_option).value)
+ System.out.println(options.check_name(get_option).value)
if (export_file != "")
File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
if (get_option == "" && export_file == "")
- java.lang.System.out.println(options.print)
+ System.out.println(options.print)
0
case _ => error("Bad arguments:\n" + cat_lines(args))
--- a/src/Pure/System/platform.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/System/platform.scala Thu Feb 20 21:45:08 2014 +0100
@@ -7,7 +7,6 @@
package isabelle
-import java.lang.System
import scala.util.matching.Regex
--- a/src/Pure/System/session.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/System/session.scala Thu Feb 20 21:45:08 2014 +0100
@@ -8,7 +8,6 @@
package isabelle
-import java.lang.System
import java.util.{Timer, TimerTask}
import scala.collection.mutable
--- a/src/Pure/Thy/html.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Thy/html.scala Thu Feb 20 21:45:08 2014 +0100
@@ -7,6 +7,7 @@
package isabelle
+
import scala.collection.mutable.ListBuffer
--- a/src/Pure/Thy/thy_load.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Thy/thy_load.ML Thu Feb 20 21:45:08 2014 +0100
@@ -199,7 +199,7 @@
val _ =
if not do_check orelse File.exists path then ()
else error ("Bad file: " ^ Path.print (Path.expand path) ^ Position.here pos);
- val _ = Position.report pos (Markup.path name);
+ val _ = Context_Position.report ctxt pos (Markup.path name);
in
space_explode "/" name
|> map Thy_Output.verb_text
--- a/src/Pure/Thy/thy_output.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML Thu Feb 20 21:45:08 2014 +0100
@@ -523,7 +523,7 @@
(case find_first (fn thy => Context.theory_name thy = name)
(Theory.nodes_of (Proof_Context.theory_of ctxt)) of
NONE => error ("No ancestor theory " ^ quote name ^ Position.here pos)
- | SOME thy => (Position.report pos (Theory.get_markup thy); Pretty.str name));
+ | SOME thy => (Context_Position.report ctxt pos (Theory.get_markup thy); Pretty.str name));
(* default output *)
@@ -670,6 +670,6 @@
val _ = Theory.setup
(antiquotation (Binding.name "url") (Scan.lift (Parse.position Parse.name))
(fn {context = ctxt, ...} => fn (name, pos) =>
- (Position.report pos (Markup.url name); enclose "\\url{" "}" name)));
+ (Context_Position.report ctxt pos (Markup.url name); enclose "\\url{" "}" name)));
end;
--- a/src/Pure/Tools/build.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Tools/build.scala Thu Feb 20 21:45:08 2014 +0100
@@ -33,7 +33,7 @@
class Console_Progress(verbose: Boolean) extends Progress
{
- override def echo(msg: String) { java.lang.System.out.println(msg) }
+ override def echo(msg: String) { System.out.println(msg) }
override def theory(session: String, theory: String): Unit =
if (verbose) echo(session + ": theory " + theory)
@@ -744,7 +744,7 @@
def ignore_error(msg: String): (List[Properties.T], Double) =
{
- java.lang.System.err.println("### Ignoring bad log file: " + path +
+ System.err.println("### Ignoring bad log file: " + path +
(if (msg == "") "" else "\n" + msg))
(Nil, 0.0)
}
--- a/src/Pure/Tools/keywords.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Tools/keywords.scala Thu Feb 20 21:45:08 2014 +0100
@@ -142,7 +142,7 @@
}
val file = if (name == "") "isar-keywords.el" else "isar-keywords-" + name + ".el"
- java.lang.System.err.println(file)
+ System.err.println(file)
File.write(Path.explode(file), output)
}
--- a/src/Pure/Tools/main.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Tools/main.scala Thu Feb 20 21:45:08 2014 +0100
@@ -7,7 +7,7 @@
package isabelle
-import java.lang.{System, Class, ClassLoader}
+import java.lang.{Class, ClassLoader}
import java.io.{File => JFile, BufferedReader, InputStreamReader}
import java.nio.file.Files
--- a/src/Pure/Tools/rail.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Tools/rail.ML Thu Feb 20 21:45:08 2014 +0100
@@ -39,6 +39,10 @@
fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
+fun reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
+ | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports antiq
+ | reports_of_token _ = [];
+
(* stopper *)
@@ -71,7 +75,8 @@
Antiquote.scan_antiq >> (fn antiq as (ss, _) => token (Antiq antiq) ss) ||
scan_keyword >> (token Keyword o single) ||
Lexicon.scan_id >> token Ident ||
- Symbol_Pos.scan_string_q err_prefix >> (token String o #1 o #2);
+ Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
+ [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
val scan =
(Scan.repeat scan_token >> flat) --|
@@ -80,7 +85,7 @@
in
-val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan) o Symbol_Pos.explode;
+val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan);
end;
@@ -187,8 +192,12 @@
in
-val read =
- #1 o Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) o tokenize;
+fun read ctxt (s, pos) =
+ let
+ val _ = Context_Position.report ctxt pos Markup.language_rail;
+ val toks = tokenize (Symbol_Pos.explode (s, pos));
+ val _ = Context_Position.reports ctxt (maps reports_of_token toks);
+ in #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks) end;
end;
@@ -267,7 +276,7 @@
val _ = Theory.setup
(Thy_Output.antiquotation @{binding rail}
(Scan.lift (Parse.source_position (Parse.string || Parse.cartouche)))
- (fn {state, ...} => output_rules state o read));
+ (fn {state, context, ...} => output_rules state o read context));
end;
--- a/src/Pure/Tools/simplifier_trace.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML Thu Feb 20 21:45:08 2014 +0100
@@ -140,7 +140,6 @@
fun output_result (id, data) =
Output.result (Markup.serial_properties id) data
-val serialN = "serial"
val parentN = "parent"
val textN = "text"
val memoryN = "memory"
--- a/src/Pure/display.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/display.ML Thu Feb 20 21:45:08 2014 +0100
@@ -55,22 +55,21 @@
val th = Thm.strip_shyps raw_th;
val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
- val xshyps = Thm.extra_shyps th;
+ val hyps' = if show_hyps then hyps else Thm.undeclared_hyps (Context.Proof ctxt) th;
+ val extra_shyps = Thm.extra_shyps th;
val tags = Thm.get_tags th;
val q = if quote then Pretty.quote else I;
val prt_term = q o Syntax.pretty_term ctxt;
- val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
- val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps;
- val hlen = length xshyps + length hyps' + length tpairs;
+ val hlen = length extra_shyps + length hyps' + length tpairs;
val hsymbs =
if hlen = 0 then []
else if show_hyps orelse show_hyps' then
[Pretty.brk 2, Pretty.list "[" "]"
(map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
- map (Syntax.pretty_sort ctxt) xshyps)]
+ map (Syntax.pretty_sort ctxt) extra_shyps)]
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
val tsymbs =
if null tags orelse not show_tags then []
--- a/src/Pure/more_thm.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/more_thm.ML Thu Feb 20 21:45:08 2014 +0100
@@ -55,6 +55,7 @@
val assume_hyps: cterm -> Proof.context -> thm * Proof.context
val unchecked_hyps: Proof.context -> Proof.context
val restore_hyps: Proof.context -> Proof.context -> Proof.context
+ val undeclared_hyps: Context.generic -> thm -> term list
val check_hyps: Context.generic -> thm -> thm
val elim_implies: thm -> thm -> thm
val forall_elim_var: int -> thm -> thm
@@ -281,26 +282,26 @@
val unchecked_hyps = (Hyps.map o apsnd) (K false);
fun restore_hyps ctxt = (Hyps.map o apsnd) (K (#2 (Hyps.get ctxt)));
+fun undeclared_hyps context th =
+ Thm.hyps_of th
+ |> filter_out
+ (case context of
+ Context.Theory _ => K false
+ | Context.Proof ctxt =>
+ (case Hyps.get ctxt of
+ (_, false) => K true
+ | (hyps, _) => Termtab.defined hyps));
+
fun check_hyps context th =
- let
- val declared_hyps =
- (case context of
- Context.Theory _ => K false
- | Context.Proof ctxt =>
- (case Hyps.get ctxt of
- (_, false) => K true
- | (hyps, _) => Termtab.defined hyps));
- val undeclared = filter_out declared_hyps (Thm.hyps_of th);
- in
- if null undeclared then th
- else
+ (case undeclared_hyps context th of
+ [] => th
+ | undeclared =>
let
val ctxt = Context.cases Syntax.init_pretty_global I context;
in
error (Pretty.string_of (Pretty.big_list "Undeclared hyps:"
(map (Pretty.item o single o Syntax.pretty_term ctxt) undeclared)))
- end
- end;
+ end);
--- a/src/Pure/raw_simplifier.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/raw_simplifier.ML Thu Feb 20 21:45:08 2014 +0100
@@ -1082,18 +1082,19 @@
(case term_of t0 of
Abs (a, T, _) =>
let
- val (b, ctxt') = Variable.next_bound (a, T) ctxt;
- val (v, t') = Thm.dest_abs (SOME b) t0;
- val b' = #1 (Term.dest_Free (term_of v));
+ val (v, ctxt') = Variable.next_bound (a, T) ctxt;
+ val b = #1 (Term.dest_Free v);
+ val (v', t') = Thm.dest_abs (SOME b) t0;
+ val b' = #1 (Term.dest_Free (term_of v'));
val _ =
if b <> b' then
- warning ("Simplifier: renamed bound variable " ^
+ warning ("Bad Simplifier context: renamed bound variable " ^
quote b ^ " to " ^ quote b' ^ Position.here (Position.thread_data ()))
else ();
val skel' = (case skel of Abs (_, _, sk) => sk | _ => skel0);
in
(case botc skel' ctxt' t' of
- SOME thm => SOME (Thm.abstract_rule a v thm)
+ SOME thm => SOME (Thm.abstract_rule a v' thm)
| NONE => NONE)
end
| t $ _ =>
--- a/src/Pure/variable.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Pure/variable.ML Thu Feb 20 21:45:08 2014 +0100
@@ -32,7 +32,7 @@
val lookup_const: Proof.context -> string -> string option
val is_const: Proof.context -> string -> bool
val declare_const: string * string -> Proof.context -> Proof.context
- val next_bound: string * typ -> Proof.context -> string * Proof.context
+ val next_bound: string * typ -> Proof.context -> term * Proof.context
val revert_bounds: Proof.context -> term -> term
val is_fixed: Proof.context -> string -> bool
val newly_fixed: Proof.context -> Proof.context -> string -> bool
@@ -313,7 +313,7 @@
let
val b = Name.bound (#1 (#bounds (rep_data ctxt)));
val ctxt' = ctxt |> map_bounds (fn (next, bounds) => (next + 1, ((b, T), a) :: bounds));
- in (b, ctxt') end;
+ in (Free (b, T), ctxt') end;
fun revert_bounds ctxt t =
(case #2 (#bounds (rep_data ctxt)) of
--- a/src/Tools/Graphview/src/graph_panel.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/Graphview/src/graph_panel.scala Thu Feb 20 21:45:08 2014 +0100
@@ -6,6 +6,7 @@
package isabelle.graphview
+
import isabelle._
import java.awt.{Dimension, Graphics2D, Point, Rectangle}
--- a/src/Tools/Graphview/src/model.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/Graphview/src/model.scala Thu Feb 20 21:45:08 2014 +0100
@@ -9,6 +9,7 @@
import isabelle._
import isabelle.graphview.Mutators._
+
import java.awt.Color
--- a/src/Tools/Graphview/src/mutator_dialog.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/Graphview/src/mutator_dialog.scala Thu Feb 20 21:45:08 2014 +0100
@@ -6,6 +6,7 @@
package isabelle.graphview
+
import isabelle._
import java.awt.Color
--- a/src/Tools/Graphview/src/popups.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/Graphview/src/popups.scala Thu Feb 20 21:45:08 2014 +0100
@@ -9,6 +9,7 @@
import isabelle._
import isabelle.graphview.Mutators._
+
import javax.swing.JPopupMenu
import scala.swing.{Action, Menu, MenuItem, Separator}
--- a/src/Tools/Graphview/src/visualizer.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/Graphview/src/visualizer.scala Thu Feb 20 21:45:08 2014 +0100
@@ -9,7 +9,6 @@
import isabelle._
-
import java.awt.{Font, FontMetrics, Color => JColor, Shape, RenderingHints, Graphics2D}
import java.awt.image.BufferedImage
import javax.swing.JComponent
--- a/src/Tools/coherent.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/coherent.ML Thu Feb 20 21:45:08 2014 +0100
@@ -20,10 +20,8 @@
signature COHERENT =
sig
- val verbose: bool Unsynchronized.ref
- val show_facts: bool Unsynchronized.ref
+ val trace: bool Config.T
val coherent_tac: Proof.context -> thm list -> int -> tactic
- val setup: theory -> theory
end;
functor Coherent(Data: COHERENT_DATA) : COHERENT =
@@ -31,9 +29,8 @@
(** misc tools **)
-val verbose = Unsynchronized.ref false;
-
-fun message f = if !verbose then tracing (f ()) else ();
+val (trace, trace_setup) = Attrib.config_bool @{binding coherent_trace} (K false);
+fun cond_trace ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ();
datatype cl_prf =
ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
@@ -78,7 +75,7 @@
val empty_env = (Vartab.empty, Vartab.empty);
(* Find matcher that makes conjunction valid in given state *)
-fun valid_conj ctxt facts env [] = Seq.single (env, [])
+fun valid_conj _ _ env [] = Seq.single (env, [])
| valid_conj ctxt facts env (t :: ts) =
Seq.maps (fn (u, x) => Seq.map (apsnd (cons x))
(valid_conj ctxt facts
@@ -91,118 +88,127 @@
let
val vs = fold Term.add_vars (maps snd cs) [];
fun insts [] inst = Seq.single inst
- | insts ((ixn, T) :: vs') inst = Seq.maps
- (fn t => insts vs' (((ixn, T), t) :: inst))
- (Seq.of_list (case Typtab.lookup dom T of
- NONE => error ("Unknown domain: " ^
- Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
- commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
- | SOME ts => ts))
- in Seq.map (fn inst =>
- (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
- (insts vs [])
+ | insts ((ixn, T) :: vs') inst =
+ Seq.maps (fn t => insts vs' (((ixn, T), t) :: inst))
+ (Seq.of_list
+ (case Typtab.lookup dom T of
+ NONE =>
+ error ("Unknown domain: " ^
+ Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
+ commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
+ | SOME ts => ts))
+ in
+ Seq.map (fn inst =>
+ (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
+ (insts vs [])
end;
(* Check whether disjunction is valid in given state *)
-fun is_valid_disj ctxt facts [] = false
+fun is_valid_disj _ _ [] = false
| is_valid_disj ctxt facts ((Ts, ts) :: ds) =
- let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts
- in case Seq.pull (valid_conj ctxt facts empty_env
- (map (fn t => subst_bounds (rev vs, t)) ts)) of
+ let val vs = map_index (fn (i, T) => Var (("x", i), T)) Ts in
+ (case Seq.pull (valid_conj ctxt facts empty_env
+ (map (fn t => subst_bounds (rev vs, t)) ts)) of
SOME _ => true
- | NONE => is_valid_disj ctxt facts ds
+ | NONE => is_valid_disj ctxt facts ds)
end;
-val show_facts = Unsynchronized.ref false;
-
-fun string_of_facts ctxt s facts = space_implode "\n"
- (s :: map (Syntax.string_of_term ctxt)
- (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
-
-fun print_facts ctxt facts =
- if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts)
- else ();
+fun string_of_facts ctxt s facts =
+ Pretty.string_of (Pretty.big_list s
+ (map (Syntax.pretty_term ctxt) (map fst (sort (int_ord o pairself snd) (Net.content facts)))));
fun valid ctxt rules goal dom facts nfacts nparams =
- let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
- valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
- let val cs' = map (fn (Ts, ts) =>
- (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
- in
- inst_extra_vars ctxt dom cs' |>
- Seq.map_filter (fn (inst, cs'') =>
- if is_valid_disj ctxt facts cs'' then NONE
- else SOME (th, env, inst, is, cs''))
- end))
+ let
+ val seq =
+ Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
+ valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
+ let val cs' = map (fn (Ts, ts) =>
+ (map (Envir.subst_type tye) Ts, map (Envir.subst_term env) ts)) cs
+ in
+ inst_extra_vars ctxt dom cs' |>
+ Seq.map_filter (fn (inst, cs'') =>
+ if is_valid_disj ctxt facts cs'' then NONE
+ else SOME (th, env, inst, is, cs''))
+ end));
in
- case Seq.pull seq of
- NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE)
+ (case Seq.pull seq of
+ NONE =>
+ (if Context_Position.is_visible ctxt then
+ warning (string_of_facts ctxt "Countermodel found:" facts)
+ else (); NONE)
| SOME ((th, env, inst, is, cs), _) =>
if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
else
(case valid_cases ctxt rules goal dom facts nfacts nparams cs of
- NONE => NONE
- | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs)))
+ NONE => NONE
+ | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs))))
end
-and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME []
+and valid_cases _ _ _ _ _ _ _ [] = SOME []
| valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
let
- val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
- val params = map_index (fn (i, T) =>
- Free ("par" ^ string_of_int (nparams + i), T)) Ts;
- val ts' = map_index (fn (i, t) =>
- (subst_bounds (rev params, t), nfacts + i)) ts;
- val dom' = fold (fn (T, p) =>
- Typtab.map_default (T, []) (fn ps => ps @ [p]))
- (Ts ~~ params) dom;
- val facts' = fold (fn (t, i) => Net.insert_term op =
- (t, (t, i))) ts' facts
+ val _ =
+ cond_trace ctxt (fn () =>
+ Pretty.string_of (Pretty.block
+ (Pretty.str "case" :: Pretty.brk 1 ::
+ Pretty.commas (map (Syntax.pretty_term ctxt) ts))));
+
+ val ps = map_index (fn (i, T) => ("par" ^ string_of_int (nparams + i), T)) Ts;
+ val (params, ctxt') = fold_map Variable.next_bound ps ctxt;
+ val ts' = map_index (fn (i, t) => (subst_bounds (rev params, t), nfacts + i)) ts;
+ val dom' =
+ fold (fn (T, p) => Typtab.map_default (T, []) (fn ps => ps @ [p])) (Ts ~~ params) dom;
+ val facts' = fold (fn (t, i) => Net.insert_term op = (t, (t, i))) ts' facts;
in
- case valid ctxt rules goal dom' facts'
- (nfacts + length ts) (nparams + length Ts) of
+ (case valid ctxt' rules goal dom' facts' (nfacts + length ts) (nparams + length Ts) of
NONE => NONE
- | SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
- NONE => NONE
- | SOME prfs => SOME ((params, prf) :: prfs))
+ | SOME prf =>
+ (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
+ NONE => NONE
+ | SOME prfs => SOME ((params, prf) :: prfs)))
end;
(** proof replaying **)
-fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
+fun thm_of_cl_prf ctxt goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
let
- val _ = message (fn () => space_implode "\n"
- ("asms:" :: map (Display.string_of_thm_global thy) asms) ^ "\n\n");
- val th' = Drule.implies_elim_list
- (Thm.instantiate
- (map (fn (ixn, (S, T)) =>
- (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
- (Vartab.dest tye),
- map (fn (ixn, (T, t)) =>
- (Thm.cterm_of thy (Var (ixn, Envir.subst_type tye T)),
- Thm.cterm_of thy t)) (Vartab.dest env) @
- map (fn (ixnT, t) =>
- (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
- (map (nth asms) is);
- val (_, cases) = dest_elim (prop_of th')
+ val thy = Proof_Context.theory_of ctxt;
+ val cert = Thm.cterm_of thy;
+ val certT = Thm.ctyp_of thy;
+ val _ =
+ cond_trace ctxt (fn () =>
+ Pretty.string_of (Pretty.big_list "asms:" (map (Display.pretty_thm ctxt) asms)));
+ val th' =
+ Drule.implies_elim_list
+ (Thm.instantiate
+ (map (fn (ixn, (S, T)) => (certT (TVar ((ixn, S))), certT T)) (Vartab.dest tye),
+ map (fn (ixn, (T, t)) =>
+ (cert (Var (ixn, Envir.subst_type tye T)), cert t)) (Vartab.dest env) @
+ map (fn (ixnT, t) => (cert (Var ixnT), cert t)) insts) th)
+ (map (nth asms) is);
+ val (_, cases) = dest_elim (prop_of th');
in
- case (cases, prfs) of
+ (case (cases, prfs) of
([([], [_])], []) => th'
- | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf
- | _ => Drule.implies_elim_list
- (Thm.instantiate (Thm.match
- (Drule.strip_imp_concl (cprop_of th'), goal)) th')
- (map (thm_of_case_prf thy goal asms) (prfs ~~ cases))
+ | ([([], [_])], [([], prf)]) => thm_of_cl_prf ctxt goal (asms @ [th']) prf
+ | _ =>
+ Drule.implies_elim_list
+ (Thm.instantiate (Thm.match
+ (Drule.strip_imp_concl (cprop_of th'), goal)) th')
+ (map (thm_of_case_prf ctxt goal asms) (prfs ~~ cases)))
end
-and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) =
+and thm_of_case_prf ctxt goal asms ((params, prf), (_, asms')) =
let
- val cparams = map (cterm_of thy) params;
- val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms'
+ val thy = Proof_Context.theory_of ctxt;
+ val cert = Thm.cterm_of thy;
+ val cparams = map cert params;
+ val asms'' = map (cert o curry subst_bounds (rev params)) asms';
+ val (prems'', ctxt') = fold_map Thm.assume_hyps asms'' ctxt;
in
- Drule.forall_intr_list cparams (Drule.implies_intr_list asms''
- (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
+ Drule.forall_intr_list cparams
+ (Drule.implies_intr_list asms'' (thm_of_cl_prf ctxt' goal (asms @ prems'') prf))
end;
@@ -211,20 +217,24 @@
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
- let val xs = map (term_of o #2) params @
- map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
- (rev (Variable.dest_fixes ctxt'')) (* FIXME !? *)
+ let
+ val xs =
+ map (term_of o #2) params @
+ map (fn (_, s) => Free (s, the (Variable.default_type ctxt'' s)))
+ (rev (Variable.dest_fixes ctxt'')) (* FIXME !? *)
in
- case valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
- (mk_dom xs) Net.empty 0 0 of
- NONE => no_tac
- | SOME prf =>
- rtac (thm_of_cl_prf (Proof_Context.theory_of ctxt'') concl [] prf) 1
+ (case
+ valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
+ (mk_dom xs) Net.empty 0 0 of
+ NONE => no_tac
+ | SOME prf => rtac (thm_of_cl_prf ctxt'' concl [] prf) 1)
end) ctxt' 1) ctxt;
-val setup = Method.setup @{binding coherent}
- (Attrib.thms >> (fn rules => fn ctxt =>
- METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
- "prove coherent formula";
+val _ = Theory.setup
+ (trace_setup #>
+ Method.setup @{binding coherent}
+ (Attrib.thms >> (fn rules => fn ctxt =>
+ METHOD (fn facts => HEADGOAL (coherent_tac ctxt (facts @ rules)))))
+ "prove coherent formula");
end;
--- a/src/Tools/cong_tac.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/cong_tac.ML Thu Feb 20 21:45:08 2014 +0100
@@ -21,14 +21,15 @@
_ $ (_ $ (f $ x) $ (g $ y)) =>
let
val cong' = Thm.lift_rule cgoal cong;
- val _ $ (_ $ (f' $ x') $ (g' $ y')) =
- Logic.strip_assums_concl (Thm.prop_of cong');
+ val _ $ (_ $ (f' $ x') $ (g' $ y')) = Logic.strip_assums_concl (Thm.prop_of cong');
val ps = Logic.strip_params (Thm.concl_of cong');
- val insts = [(f', f), (g', g), (x', x), (y', y)]
+ val insts =
+ [(f', f), (g', g), (x', x), (y', y)]
|> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
in
- fn st => compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
- handle THM _ => no_tac st
+ fn st =>
+ compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
+ handle THM _ => no_tac st
end
| _ => no_tac)
end);
--- a/src/Tools/intuitionistic.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/intuitionistic.ML Thu Feb 20 21:45:08 2014 +0100
@@ -42,17 +42,20 @@
REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
REMDUPS (unsafe_step_tac ctxt) i;
-fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else
- let
- val ps = Logic.strip_assums_hyp g;
- val c = Logic.strip_assums_concl g;
- in
- if member (fn ((ps1, c1), (ps2, c2)) =>
- c1 aconv c2 andalso
- length ps1 = length ps2 andalso
- eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
- else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
- end);
+fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) =>
+ if d > lim then no_tac
+ else
+ let
+ val ps = Logic.strip_assums_hyp g;
+ val c = Logic.strip_assums_concl g;
+ in
+ if member (fn ((ps1, c1), (ps2, c2)) =>
+ c1 aconv c2 andalso
+ length ps1 = length ps2 andalso
+ eq_set (op aconv) (ps1, ps2)) gs (ps, c)
+ then no_tac
+ else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
+ end);
in
Binary file src/Tools/jEdit/PIDE.png has changed
--- a/src/Tools/jEdit/src/completion_popup.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Thu Feb 20 21:45:08 2014 +0100
@@ -110,7 +110,13 @@
val history = PIDE.completion_history.value
val decode = Isabelle_Encoding.is_active(buffer)
- syntax.completion.complete(history, decode, explicit, text) match {
+ val context =
+ (PIDE.document_view(text_area) match {
+ case None => None
+ case Some(doc_view) => doc_view.get_rendering().completion_context(caret)
+ }) getOrElse syntax.completion_context
+
+ syntax.completion.complete(history, decode, explicit, text, context) match {
case Some(result) =>
if (result.unique && result.items.head.immediate && immediate)
insert(result.items.head)
@@ -277,7 +283,8 @@
val caret = text_field.getCaret.getDot
val text = text_field.getText.substring(0, caret)
- syntax.completion.complete(history, decode = true, explicit = false, text) match {
+ syntax.completion.complete(
+ history, decode = true, explicit = false, text, syntax.completion_context) match {
case Some(result) =>
val fm = text_field.getFontMetrics(text_field.getFont)
val loc =
--- a/src/Tools/jEdit/src/document_view.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Thu Feb 20 21:45:08 2014 +0100
@@ -243,7 +243,7 @@
}
case bad =>
- java.lang.System.err.println("command_change_actor: ignoring bad message " + bad)
+ System.err.println("command_change_actor: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/find_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/find_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -77,7 +77,7 @@
Swing_Thread.later { handle_resize() }
case bad =>
- java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
+ System.err.println("Find_Dockable: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/info_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -14,7 +14,6 @@
import scala.swing.Button
import scala.swing.event.ButtonClicked
-import java.lang.System
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
--- a/src/Tools/jEdit/src/isabelle.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Thu Feb 20 21:45:08 2014 +0100
@@ -31,7 +31,12 @@
"isabelle-output", // pretty text area output
"isabelle-root") // session ROOT
- private lazy val symbols_syntax = Outer_Syntax.init().no_tokens
+ private lazy val ml_syntax: Outer_Syntax =
+ Outer_Syntax.init().no_tokens.
+ set_completion_context(Completion.Context(Markup.Language.ML, false))
+
+ private lazy val news_syntax: Outer_Syntax =
+ Outer_Syntax.init().no_tokens
def mode_syntax(name: String): Option[Outer_Syntax] =
name match {
@@ -40,7 +45,8 @@
if (syntax == Outer_Syntax.empty) None else Some(syntax)
case "isabelle-options" => Some(Options.options_syntax)
case "isabelle-root" => Some(Build.root_syntax)
- case "isabelle-ml" | "isabelle-news" => Some(symbols_syntax)
+ case "isabelle-ml" => Some(ml_syntax)
+ case "isabelle-news" => Some(news_syntax)
case "isabelle-output" => None
case _ => None
}
--- a/src/Tools/jEdit/src/monitor_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -46,7 +46,7 @@
delay_update.invoke()
}
- case bad => java.lang.System.err.println("Monitor_Dockable: ignoring bad message " + bad)
+ case bad => System.err.println("Monitor_Dockable: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -14,7 +14,6 @@
import scala.swing.{Button, CheckBox}
import scala.swing.event.ButtonClicked
-import java.lang.System
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
--- a/src/Tools/jEdit/src/plugin.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Feb 20 21:45:08 2014 +0100
@@ -142,6 +142,27 @@
Document_View.exit(text_area)
}
}
+
+
+ /* current document content */
+
+ def snapshot(view: View): Document.Snapshot =
+ {
+ val buffer = view.getBuffer
+ document_model(buffer) match {
+ case Some(model) => model.snapshot
+ case None => error("No document model for current buffer")
+ }
+ }
+
+ def rendering(view: View): Rendering =
+ {
+ val text_area = view.getTextArea
+ document_view(text_area) match {
+ case Some(doc_view) => doc_view.get_rendering()
+ case None => error("No document view for current text area")
+ }
+ }
}
@@ -233,7 +254,7 @@
case _ =>
}
- case bad => java.lang.System.err.println("session_manager: ignoring bad message " + bad)
+ case bad => System.err.println("session_manager: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/protocol_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -9,8 +9,6 @@
import isabelle._
-import java.lang.System
-
import scala.actors.Actor._
import scala.swing.{TextArea, ScrollPane}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -9,8 +9,6 @@
import isabelle._
-import java.lang.System
-
import scala.actors.Actor._
import scala.swing.{TextArea, ScrollPane}
--- a/src/Tools/jEdit/src/rendering.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Thu Feb 20 21:45:08 2014 +0100
@@ -200,11 +200,39 @@
val dynamic_color = color_value("dynamic_color")
- /* command overview */
+ /* completion context */
+
+ private val completion_elements =
+ Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE,
+ Markup.COMMENT, Markup.LANGUAGE, Markup.ML_STRING, Markup.ML_COMMENT)
+
+ def completion_context(caret: Text.Offset): Option[Completion.Context] =
+ if (caret > 0) {
+ val result =
+ snapshot.select_markup(Text.Range(caret - 1, caret + 1), completion_elements, _ =>
+ {
+ case Text.Info(_, elem)
+ if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
+ Some(Completion.Context(Markup.Language.ML, true))
+ case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
+ Some(Completion.Context(language, symbols))
+ case Text.Info(_, XML.Elem(markup, _)) =>
+ Some(Completion.Context(Markup.Language.UNKNOWN, true))
+ })
+ result match {
+ case Text.Info(_, context) :: _ => Some(context)
+ case Nil => None
+ }
+ }
+ else None
+
+
+ /* command status overview */
val overview_limit = options.int("jedit_text_overview_limit")
- private val overview_include = Protocol.command_status_markup + Markup.WARNING + Markup.ERROR
+ private val overview_elements =
+ Protocol.command_status_markup + Markup.WARNING + Markup.ERROR
def overview_color(range: Text.Range): Option[Color] =
{
@@ -212,14 +240,13 @@
else {
val results =
snapshot.cumulate_markup[(Protocol.Status, Int)](
- range, (Protocol.Status.init, 0), Some(overview_include), _ =>
+ range, (Protocol.Status.init, 0), overview_elements, _ =>
{
case ((status, pri), Text.Info(_, elem)) =>
- if (elem.name == Markup.WARNING || elem.name == Markup.ERROR)
+ if (Protocol.command_status_markup(elem.name))
+ Some((Protocol.command_status(status, elem.markup), pri))
+ else
Some((status, pri max Rendering.message_pri(elem.name)))
- else if (overview_include(elem.name))
- Some((Protocol.command_status(status, elem.markup), pri))
- else None
})
if (results.isEmpty) None
else {
@@ -238,9 +265,9 @@
}
- /* markup selectors */
+ /* highlighted area */
- private val highlight_include =
+ private val highlight_elements =
Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE,
Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
@@ -248,17 +275,17 @@
def highlight(range: Text.Range): Option[Text.Info[Color]] =
{
- snapshot.select_markup(range, Some(highlight_include), _ =>
- {
- case Text.Info(info_range, elem) =>
- if (highlight_include(elem.name))
- Some(Text.Info(snapshot.convert(info_range), highlight_color))
- else None
- }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
+ snapshot.select_markup(range, highlight_elements, _ =>
+ {
+ case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
+ }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
}
- private val hyperlink_include = Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
+ /* hyperlinks */
+
+ private val hyperlink_elements =
+ Set(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL)
private def hyperlink_file(line: Int, name: String): Option[PIDE.editor.Hyperlink] =
if (Path.is_ok(name))
@@ -276,18 +303,18 @@
def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
- snapshot.cumulate_markup[List[Text.Info[PIDE.editor.Hyperlink]]](
- range, Nil, Some(hyperlink_include), _ =>
+ snapshot.cumulate_markup[Vector[Text.Info[PIDE.editor.Hyperlink]]](
+ range, Vector.empty, hyperlink_elements, _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
val link = PIDE.editor.hyperlink_file(jedit_file)
- Some(Text.Info(snapshot.convert(info_range), link) :: links)
+ Some(links :+ Text.Info(snapshot.convert(info_range), link))
case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
val link = PIDE.editor.hyperlink_url(name)
- Some(Text.Info(snapshot.convert(info_range), link) :: links)
+ Some(links :+ Text.Info(snapshot.convert(info_range), link))
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
if !props.exists(
@@ -301,7 +328,7 @@
case Position.Def_Id_Offset(id, offset) => hyperlink_command(id, offset)
case _ => None
}
- opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
+ opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
val opt_link =
@@ -310,45 +337,53 @@
case Position.Id_Offset(id, offset) => hyperlink_command(id, offset)
case _ => None
}
- opt_link.map(link => (Text.Info(snapshot.convert(info_range), link) :: links))
+ opt_link.map(link => links :+ (Text.Info(snapshot.convert(info_range), link)))
case _ => None
- }) match { case Text.Info(_, info :: _) :: _ => Some(info) case _ => None }
+ }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
}
- private val active_include =
- Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
+ /* active elements */
+
+ private val active_elements =
+ Set(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.SIMP_TRACE)
def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
- snapshot.select_markup(range, Some(active_include), command_state =>
- {
- case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
- if !command_state.results.defined(serial) =>
- Some(Text.Info(snapshot.convert(info_range), elem))
- case Text.Info(info_range, elem) =>
- if (elem.name == Markup.BROWSER ||
- elem.name == Markup.GRAPHVIEW ||
- elem.name == Markup.SENDBACK ||
- elem.name == Markup.SIMP_TRACE)
- Some(Text.Info(snapshot.convert(info_range), elem))
- else None
- }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
+ snapshot.select_markup(range, active_elements, command_state =>
+ {
+ case Text.Info(info_range, elem) =>
+ if (elem.name == Markup.DIALOG) {
+ elem match {
+ case Protocol.Dialog(_, serial, _)
+ if !command_state.results.defined(serial) =>
+ Some(Text.Info(snapshot.convert(info_range), elem))
+ case _ => None
+ }
+ }
+ else Some(Text.Info(snapshot.convert(info_range), elem))
+ }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
def command_results(range: Text.Range): Command.Results =
{
val results =
- snapshot.select_markup[Command.Results](range, None, command_state =>
+ snapshot.select_markup[Command.Results](range, _ => true, command_state =>
{ case _ => Some(command_state.results) }).map(_.info)
(Command.Results.empty /: results)(_ ++ _)
}
+
+ /* tooltip messages */
+
+ private val tooltip_message_elements =
+ Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
+
def tooltip_message(range: Text.Range): Option[Text.Info[XML.Body]] =
{
val results =
- snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](range, Nil,
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
+ snapshot.cumulate_markup[List[Text.Info[Command.Results.Entry]]](
+ range, Nil, tooltip_message_elements, _ =>
{
case (msgs, Text.Info(info_range,
XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
@@ -373,6 +408,8 @@
}
+ /* tooltips */
+
private val tooltips: Map[String, String] =
Map(
Markup.TOKEN_RANGE -> "inner syntax token",
@@ -395,17 +432,19 @@
def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
{
- def add(prev: Text.Info[(Timing, List[(Boolean, XML.Tree)])],
- r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, List[(Boolean, XML.Tree)])] =
+ def add(prev: Text.Info[(Timing, Vector[(Boolean, XML.Tree)])],
+ r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, Vector[(Boolean, XML.Tree)])] =
{
val r = snapshot.convert(r0)
val (t, info) = prev.info
- if (prev.range == r) Text.Info(r, (t, p :: info)) else Text.Info(r, (t, List(p)))
+ if (prev.range == r)
+ Text.Info(r, (t, info :+ p))
+ else Text.Info(r, (t, Vector(p)))
}
val results =
- snapshot.cumulate_markup[Text.Info[(Timing, List[(Boolean, XML.Tree)])]](
- range, Text.Info(range, (Timing.zero, Nil)), Some(tooltip_elements), _ =>
+ snapshot.cumulate_markup[Text.Info[(Timing, Vector[(Boolean, XML.Tree)])]](
+ range, Text.Info(range, (Timing.zero, Vector.empty)), tooltip_elements, _ =>
{
case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
Some(Text.Info(r, (t1 + t2, info)))
@@ -429,15 +468,15 @@
Some(add(prev, r, (true, pretty_typing("::", body))))
case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
Some(add(prev, r, (false, pretty_typing("ML:", body))))
- case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) =>
- Some(add(prev, r, (true, XML.Text("language: " + name))))
+ case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) =>
+ Some(add(prev, r, (true, XML.Text("language: " + language))))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
if (tooltips.isDefinedAt(name))
Some(add(prev, r, (true, XML.Text(tooltips(name)))))
else None
}).map(_.info)
- results.map(_.info).flatMap(_._2) match {
+ results.map(_.info).flatMap(res => res._2.toList) match {
case Nil => None
case tips =>
val r = Text.Range(results.head.range.start, results.last.range.stop)
@@ -452,18 +491,21 @@
lazy val tooltip_detach_icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
+ /* gutter icons */
+
private lazy val gutter_icons = Map(
Rendering.information_pri -> JEdit_Lib.load_icon(options.string("gutter_information_icon")),
Rendering.warning_pri -> JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
Rendering.legacy_pri -> JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
Rendering.error_pri -> JEdit_Lib.load_icon(options.string("gutter_error_icon")))
- private val gutter_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ private val gutter_elements =
+ Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
def gutter_message(range: Text.Range): Option[Icon] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, Some(gutter_elements), _ =>
+ snapshot.cumulate_markup[Int](range, 0, gutter_elements, _ =>
{
case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
@@ -484,25 +526,26 @@
}
+ /* squiggly underline */
+
private val squiggly_colors = Map(
Rendering.writeln_pri -> writeln_color,
Rendering.information_pri -> information_color,
Rendering.warning_pri -> warning_color,
Rendering.error_pri -> error_color)
- private val squiggly_include = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+ private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, Some(squiggly_include), _ =>
+ snapshot.cumulate_markup[Int](range, 0, squiggly_elements, _ =>
{
case (pri, Text.Info(_, elem)) =>
if (Protocol.is_information(elem))
Some(pri max Rendering.information_pri)
- else if (squiggly_include.contains(elem.name))
+ else
Some(pri max Rendering.message_pri(elem.name))
- else None
})
for {
Text.Info(r, pri) <- results
@@ -511,6 +554,8 @@
}
+ /* message output */
+
private val message_colors = Map(
Rendering.writeln_pri -> writeln_message_color,
Rendering.information_pri -> information_message_color,
@@ -525,38 +570,36 @@
def line_background(range: Text.Range): Option[(Color, Boolean)] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
+ snapshot.cumulate_markup[Int](range, 0, line_background_elements, _ =>
{
case (pri, Text.Info(_, elem)) =>
- val name = elem.name
- if (name == Markup.INFORMATION)
+ if (elem.name == Markup.INFORMATION)
Some(pri max Rendering.information_pri)
- else if (name == Markup.WRITELN_MESSAGE || name == Markup.TRACING_MESSAGE ||
- elem.name == Markup.WARNING_MESSAGE || name == Markup.ERROR_MESSAGE)
- Some(pri max Rendering.message_pri(name))
- else None
+ else
+ Some(pri max Rendering.message_pri(elem.name))
})
val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
- val is_separator = pri > 0 &&
- snapshot.cumulate_markup[Boolean](range, false, Some(Set(Markup.SEPARATOR)), _ =>
+ val is_separator =
+ pri > 0 &&
+ snapshot.cumulate_markup[Boolean](range, false, Set(Markup.SEPARATOR), _ =>
{
- case (_, Text.Info(_, elem)) =>
- if (elem.name == Markup.SEPARATOR) Some(true) else None
+ case _ => Some(true)
}).exists(_.info)
message_colors.get(pri).map((_, is_separator))
}
-
def output_messages(st: Command.State): List[XML.Tree] =
st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
- private val background1_include =
+ /* text background */
+
+ private val background1_elements =
Protocol.command_status_markup + Markup.WRITELN_MESSAGE + Markup.TRACING_MESSAGE +
Markup.WARNING_MESSAGE + Markup.ERROR_MESSAGE + Markup.BAD + Markup.INTENSIFY ++
- active_include
+ active_elements
def background1(range: Text.Range): List[Text.Info[Color]] =
{
@@ -565,7 +608,7 @@
for {
Text.Info(r, result) <-
snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
- range, (Some(Protocol.Status.init), None), Some(background1_include), command_state =>
+ range, (Some(Protocol.Status.init), None), background1_elements, command_state =>
{
case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
if (Protocol.command_status_markup(markup.name)) =>
@@ -582,7 +625,7 @@
Some((None, Some(active_color)))
}
case (_, Text.Info(_, elem)) =>
- if (active_include(elem.name)) Some((None, Some(active_color)))
+ if (active_elements(elem.name)) Some((None, Some(active_color)))
else None
})
color <-
@@ -596,35 +639,24 @@
} yield Text.Info(r, color)
}
+ def background2(range: Text.Range): List[Text.Info[Color]] =
+ snapshot.select_markup(range, Set(Markup.TOKEN_RANGE), _ => _ => Some(light_color))
- def background2(range: Text.Range): List[Text.Info[Color]] =
- snapshot.select_markup(range, Some(Set(Markup.TOKEN_RANGE)), _ =>
+
+ /* text foreground */
+
+ private val foreground_elements =
+ Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
+
+ def foreground(range: Text.Range): List[Text.Info[Color]] =
+ snapshot.select_markup(range, foreground_elements, _ =>
{
case Text.Info(_, elem) =>
- if (elem.name == Markup.TOKEN_RANGE) Some(light_color) else None
+ if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color) else Some(quoted_color)
})
- def bullet(range: Text.Range): List[Text.Info[Color]] =
- snapshot.select_markup(range, Some(Set(Markup.BULLET)), _ =>
- {
- case Text.Info(_, elem) =>
- if (elem.name == Markup.BULLET) Some(bullet_color) else None
- })
-
-
- private val foreground_include =
- Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED)
-
- def foreground(range: Text.Range): List[Text.Info[Color]] =
- snapshot.select_markup(range, Some(foreground_include), _ =>
- {
- case Text.Info(_, elem) =>
- if (elem.name == Markup.ANTIQUOTED) Some(antiquoted_color)
- else if (foreground_include.contains(elem.name)) Some(quoted_color)
- else None
- })
-
+ /* text color */
private val text_colors: Map[String, Color] = Map(
Markup.KEYWORD1 -> keyword1_color,
@@ -661,21 +693,27 @@
{
if (color == Token_Markup.hidden_color) List(Text.Info(range, color))
else
- snapshot.cumulate_markup(range, color, Some(text_color_elements), _ =>
+ snapshot.cumulate_markup(range, color, text_color_elements, _ =>
{
case (_, Text.Info(_, elem)) => text_colors.get(elem.name)
})
}
- /* nested text structure -- folds */
+ /* virtual bullets */
+
+ def bullet(range: Text.Range): List[Text.Info[Color]] =
+ snapshot.select_markup(range, Set(Markup.BULLET), _ => _ => Some(bullet_color))
- private val fold_depth_include = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
+
+ /* text folds */
+
+ private val fold_depth_elements =
+ Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
def fold_depth(range: Text.Range): List[Text.Info[Int]] =
- snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
+ snapshot.cumulate_markup[Int](range, 0, fold_depth_elements, _ =>
{
- case (depth, Text.Info(_, elem)) =>
- if (fold_depth_include(elem.name)) Some(depth + 1) else None
+ case (depth, _) => Some(depth + 1)
})
}
--- a/src/Tools/jEdit/src/scala_console.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Thu Feb 20 21:45:08 2014 +0100
@@ -14,7 +14,6 @@
import org.gjt.sp.jedit.{jEdit, JARClassLoader}
import org.gjt.sp.jedit.MiscUtilities
-import java.lang.System
import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
@@ -148,7 +147,7 @@
"The following special toplevel bindings are provided:\n" +
" view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
" console -- jEdit Console plugin\n" +
- " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.document_model)\n")
+ " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n")
}
override def printPrompt(console: Console, out: Output)
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -104,7 +104,7 @@
Swing_Thread.later { update_provers() }
case bad =>
- java.lang.System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
+ System.err.println("Sledgehammer_Dockable: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/syslog_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -40,7 +40,7 @@
case output: Isabelle_Process.Output =>
if (output.is_syslog) Swing_Thread.later { update_syslog() }
- case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
+ case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -14,7 +14,6 @@
ScrollPane, Component, CheckBox, BorderPanel}
import scala.swing.event.{MouseClicked, MouseMoved}
-import java.lang.System
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
import javax.swing.{JList, BorderFactory}
import javax.swing.border.{BevelBorder, SoftBevelBorder}
--- a/src/Tools/jEdit/src/timing_dockable.scala Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Thu Feb 20 21:45:08 2014 +0100
@@ -13,7 +13,6 @@
import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
import scala.swing.event.{MouseClicked, ValueChanged}
-import java.lang.System
import java.awt.{BorderLayout, Graphics2D, Insets, Color}
import javax.swing.{JList, BorderFactory}
import javax.swing.border.{BevelBorder, SoftBevelBorder}
--- a/src/Tools/quickcheck.ML Thu Feb 20 16:56:33 2014 +0100
+++ b/src/Tools/quickcheck.ML Thu Feb 20 21:45:08 2014 +0100
@@ -83,11 +83,11 @@
structure Quickcheck : QUICKCHECK =
struct
-val quickcheckN = "quickcheck"
+val quickcheckN = "quickcheck";
-val genuineN = "genuine"
-val noneN = "none"
-val unknownN = "unknown"
+val genuineN = "genuine";
+val noneN = "none";
+val unknownN = "unknown";
(* preferences *)
@@ -103,58 +103,63 @@
(* quickcheck report *)
datatype report = Report of
- { iterations : int, raised_match_errors : int,
- satisfied_assms : int list, positive_concl_tests : int }
+ {iterations : int,
+ raised_match_errors : int,
+ satisfied_assms : int list,
+ positive_concl_tests : int};
(* Quickcheck Result *)
datatype result = Result of
- { counterexample : (bool * (string * term) list) option, evaluation_terms : (term * term) list option,
- timings : (string * int) list, reports : (int * report) list}
+ {counterexample : (bool * (string * term) list) option,
+ evaluation_terms : (term * term) list option,
+ timings : (string * int) list,
+ reports : (int * report) list};
val empty_result =
- Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []}
+ Result {counterexample = NONE, evaluation_terms = NONE, timings = [], reports = []};
-fun counterexample_of (Result r) = #counterexample r
+fun counterexample_of (Result r) = #counterexample r;
-fun found_counterexample (Result r) = is_some (#counterexample r)
+fun found_counterexample (Result r) = is_some (#counterexample r);
-fun response_of (Result r) = case (#counterexample r, #evaluation_terms r) of
+fun response_of (Result r) =
+ (case (#counterexample r, #evaluation_terms r) of
(SOME ts, SOME evals) => SOME (ts, evals)
- | (NONE, NONE) => NONE
+ | (NONE, NONE) => NONE);
-fun timings_of (Result r) = #timings r
+fun timings_of (Result r) = #timings r;
fun set_response names eval_terms (SOME (genuine, ts)) (Result r) =
- let
- val (ts1, ts2) = chop (length names) ts
- val (eval_terms', _) = chop (length ts2) eval_terms
- in
- Result {counterexample = SOME (genuine, (names ~~ ts1)),
- evaluation_terms = SOME (eval_terms' ~~ ts2),
- timings = #timings r, reports = #reports r}
- end
- | set_response _ _ NONE result = result
+ let
+ val (ts1, ts2) = chop (length names) ts
+ val (eval_terms', _) = chop (length ts2) eval_terms
+ in
+ Result {counterexample = SOME (genuine, (names ~~ ts1)),
+ evaluation_terms = SOME (eval_terms' ~~ ts2),
+ timings = #timings r, reports = #reports r}
+ end
+ | set_response _ _ NONE result = result;
fun cons_timing timing (Result r) =
Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
- timings = cons timing (#timings r), reports = #reports r}
+ timings = cons timing (#timings r), reports = #reports r};
fun cons_report size (SOME report) (Result r) =
- Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
- timings = #timings r, reports = cons (size, report) (#reports r)}
- | cons_report _ NONE result = result
+ Result {counterexample = #counterexample r, evaluation_terms = #evaluation_terms r,
+ timings = #timings r, reports = cons (size, report) (#reports r)}
+ | cons_report _ NONE result = result;
fun add_timing timing result_ref =
- Unsynchronized.change result_ref (cons_timing timing)
+ Unsynchronized.change result_ref (cons_timing timing);
fun add_report size report result_ref =
- Unsynchronized.change result_ref (cons_report size report)
+ Unsynchronized.change result_ref (cons_report size report);
fun add_response names eval_terms response result_ref =
- Unsynchronized.change result_ref (set_response names eval_terms response)
+ Unsynchronized.change result_ref (set_response names eval_terms response);
(* expectation *)
@@ -162,33 +167,33 @@
datatype expectation = No_Expectation | No_Counterexample | Counterexample;
fun merge_expectation (expect1, expect2) =
- if expect1 = expect2 then expect1 else No_Expectation
+ if expect1 = expect2 then expect1 else No_Expectation;
(*quickcheck configuration -- default parameters, test generators*)
-val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "")
-val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10)
-val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100)
-val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10)
+val batch_tester = Attrib.setup_config_string @{binding quickcheck_batch_tester} (K "");
+val size = Attrib.setup_config_int @{binding quickcheck_size} (K 10);
+val iterations = Attrib.setup_config_int @{binding quickcheck_iterations} (K 100);
+val depth = Attrib.setup_config_int @{binding quickcheck_depth} (K 10);
-val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false)
-val locale = Attrib.setup_config_string @{binding quickcheck_locale} (K "interpret expand")
-val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true)
-val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false)
-val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0)
+val no_assms = Attrib.setup_config_bool @{binding quickcheck_no_assms} (K false);
+val locale = Attrib.setup_config_string @{binding quickcheck_locale} (K "interpret expand");
+val report = Attrib.setup_config_bool @{binding quickcheck_report} (K true);
+val timing = Attrib.setup_config_bool @{binding quickcheck_timing} (K false);
+val timeout = Attrib.setup_config_real @{binding quickcheck_timeout} (K 30.0);
-val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false)
-val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false)
+val genuine_only = Attrib.setup_config_bool @{binding quickcheck_genuine_only} (K false);
+val abort_potential = Attrib.setup_config_bool @{binding quickcheck_abort_potential} (K false);
-val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false)
-val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false)
-val tag = Attrib.setup_config_string @{binding quickcheck_tag} (K "")
+val quiet = Attrib.setup_config_bool @{binding quickcheck_quiet} (K false);
+val verbose = Attrib.setup_config_bool @{binding quickcheck_verbose} (K false);
+val tag = Attrib.setup_config_string @{binding quickcheck_tag} (K "");
-val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false)
+val use_subtype = Attrib.setup_config_bool @{binding quickcheck_use_subtype} (K false);
val allow_function_inversion =
- Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false)
-val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true)
-val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3)
+ Attrib.setup_config_bool @{binding quickcheck_allow_function_inversion} (K false);
+val finite_types = Attrib.setup_config_bool @{binding quickcheck_finite_types} (K true);
+val finite_type_size = Attrib.setup_config_int @{binding quickcheck_finite_type_size} (K 3);
datatype test_params = Test_Params of
{default_type: typ list, expect : expectation};
@@ -213,13 +218,14 @@
structure Data = Generic_Data
(
type T =
- ((string * (bool Config.T * tester)) list
- * ((string * (Proof.context -> term list -> (int -> term list option) list)) list
- * ((string * (Proof.context -> term list -> (int -> bool) list)) list)))
- * test_params;
+ ((string * (bool Config.T * tester)) list *
+ ((string * (Proof.context -> term list -> (int -> term list option) list)) list *
+ ((string * (Proof.context -> term list -> (int -> bool) list)) list))) *
+ test_params;
val empty = (([], ([], [])), Test_Params {default_type = [], expect = No_Expectation});
val extend = I;
- fun merge (((testers1, (batch_generators1, batch_validators1)), params1),
+ fun merge
+ (((testers1, (batch_generators1, batch_validators1)), params1),
((testers2, (batch_generators2, batch_validators2)), params2)) : T =
((AList.merge (op =) (K true) (testers1, testers2),
(AList.merge (op =) (K true) (batch_generators1, batch_generators2),
@@ -229,11 +235,11 @@
val test_params_of = snd o Data.get o Context.Proof;
-val default_type = fst o dest_test_params o test_params_of
+val default_type = fst o dest_test_params o test_params_of;
-val expect = snd o dest_test_params o test_params_of
+val expect = snd o dest_test_params o test_params_of;
-val map_test_params = Data.map o apsnd o map_test_params'
+val map_test_params = Data.map o apsnd o map_test_params';
val add_tester = Data.map o apfst o apfst o AList.update (op =);
@@ -243,18 +249,18 @@
fun active_testers ctxt =
let
- val testers = (map snd o fst o fst o Data.get o Context.Proof) ctxt
+ val testers = map snd (fst (fst (Data.get (Context.Proof ctxt))));
in
map snd (filter (fn (active, _) => Config.get ctxt active) testers)
- end
+ end;
-fun set_active_testers [] gen_ctxt = gen_ctxt
- | set_active_testers testers gen_ctxt =
+fun set_active_testers [] context = context
+ | set_active_testers testers context =
let
- val registered_testers = (fst o fst o Data.get) gen_ctxt
+ val registered_testers = fst (fst (Data.get context));
in
fold (fn (name, (config, _)) => Config.put_generic config (member (op =) testers name))
- registered_testers gen_ctxt
+ registered_testers context
end;
@@ -281,9 +287,9 @@
end;
val mk_batch_tester =
- gen_mk_tester (fn ctxt => AList.lookup (op =) ((fst o snd o fst o Data.get o Context.Proof) ctxt));
+ gen_mk_tester (AList.lookup (op =) o fst o snd o fst o Data.get o Context.Proof);
val mk_batch_validator =
- gen_mk_tester (fn ctxt => AList.lookup (op =) ((snd o snd o fst o Data.get o Context.Proof) ctxt));
+ gen_mk_tester (AList.lookup (op =) o snd o snd o fst o Data.get o Context.Proof);
(* testing propositions *)
@@ -293,11 +299,10 @@
fun limit timeout (limit_time, is_interactive) f exc () =
if limit_time then
- TimeLimit.timeLimit timeout f ()
- handle TimeLimit.TimeOut =>
- if is_interactive then exc () else raise TimeLimit.TimeOut
- else
- f ();
+ TimeLimit.timeLimit timeout f ()
+ handle TimeLimit.TimeOut =>
+ if is_interactive then exc () else raise TimeLimit.TimeOut
+ else f ();
fun message ctxt s = if Config.get ctxt quiet then () else Output.urgent_message s;
@@ -309,11 +314,13 @@
(case active_testers ctxt of
[] => error "No active testers for quickcheck"
| testers =>
- limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
- (fn () => Par_List.get_some (fn tester =>
- tester ctxt (length testers > 1) insts goals |>
- (fn result => if exists found_counterexample result then SOME result else NONE)) testers)
- (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ());
+ limit (seconds (Config.get ctxt timeout)) (limit_time, is_interactive)
+ (fn () =>
+ Par_List.get_some (fn tester =>
+ tester ctxt (length testers > 1) insts goals |>
+ (fn result => if exists found_counterexample result then SOME result else NONE))
+ testers)
+ (fn () => (message ctxt "Quickcheck ran out of time"; NONE)) ());
fun all_axioms_of ctxt t =
let
@@ -341,7 +348,8 @@
val cs = space_explode " " s;
in
if forall (fn c => c = "expand" orelse c = "interpret") cs then cs
- else (warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
+ else
+ (warning ("Invalid quickcheck_locale setting: falling back to the default setting.");
["interpret", "expand"])
end;
@@ -370,18 +378,19 @@
(case fst (Locale.specification_of thy locale) of
NONE => []
| SOME t => the_default [] (all_axioms_of lthy t));
- val config = locale_config_of (Config.get lthy locale);
- val goals =
- (case some_locale of
- NONE => [(proto_goal, eval_terms)]
- | SOME locale =>
- fold (fn c =>
- if c = "expand" then cons (Logic.list_implies (axioms_of locale, proto_goal), eval_terms)
- else if c = "interpret" then
- append (map (fn (_, phi) =>
- (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
- (Locale.registrations_of (Context.Theory thy) (*FIXME*) locale))
- else I) config []);
+ val config = locale_config_of (Config.get lthy locale);
+ val goals =
+ (case some_locale of
+ NONE => [(proto_goal, eval_terms)]
+ | SOME locale =>
+ fold (fn c =>
+ if c = "expand" then
+ cons (Logic.list_implies (axioms_of locale, proto_goal), eval_terms)
+ else if c = "interpret" then
+ append (map (fn (_, phi) =>
+ (Morphism.term phi proto_goal, map (Morphism.term phi) eval_terms))
+ (Locale.registrations_of (Context.Theory thy) (* FIXME !? *) locale))
+ else I) config []);
val _ =
verbose_message lthy
(Pretty.string_of
@@ -396,39 +405,39 @@
fun tool_name auto = (if auto then "Auto " else "") ^ "Quickcheck";
fun pretty_counterex ctxt auto NONE =
- Pretty.str (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
+ Pretty.str (tool_name auto ^ " found no counterexample." ^ Config.get ctxt tag)
| pretty_counterex ctxt auto (SOME ((genuine, cex), eval_terms)) =
(Pretty.text_fold o Pretty.fbreaks)
- (Pretty.str (tool_name auto ^ " found a " ^
+ (Pretty.str (tool_name auto ^ " found a " ^
(if genuine then "counterexample:"
else "potentially spurious counterexample due to underspecified functions:") ^
- Config.get ctxt tag) ::
- Pretty.str "" ::
- map (fn (s, t) =>
+ Config.get ctxt tag) ::
+ Pretty.str "" ::
+ map (fn (s, t) =>
Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) (rev cex) @
- (if null eval_terms then []
- else
- Pretty.str "" :: Pretty.str "Evaluated terms:" ::
- map (fn (t, u) =>
- Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
- Syntax.pretty_term ctxt u]) (rev eval_terms)));
+ (if null eval_terms then []
+ else
+ Pretty.str "" :: Pretty.str "Evaluated terms:" ::
+ map (fn (t, u) =>
+ Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
+ Syntax.pretty_term ctxt u]) (rev eval_terms)));
(* Isar commands *)
fun read_nat s =
- (case (Library.read_int o Symbol.explode) s of
+ (case Library.read_int (Symbol.explode s) of
(k, []) =>
if k >= 0 then k
else error ("Not a natural number: " ^ s)
- | (_, _ :: _) => error ("Not a natural number: " ^ s));
+ | _ => error ("Not a natural number: " ^ s));
fun read_bool "false" = false
| read_bool "true" = true
| read_bool s = error ("Not a Boolean value: " ^ s);
fun read_real s =
- (case (Real.fromString s) of
+ (case Real.fromString s of
SOME s => s
| NONE => error ("Not a real number: " ^ s));
@@ -437,44 +446,48 @@
| read_expectation "counterexample" = Counterexample
| read_expectation s = error ("Not an expectation value: " ^ s);
-fun valid_tester_name genctxt name = AList.defined (op =) (fst (fst (Data.get genctxt))) name;
+fun valid_tester_name genctxt name =
+ AList.defined (op =) (fst (fst (Data.get genctxt))) name;
fun parse_tester name (testers, genctxt) =
if valid_tester_name genctxt name then
(insert (op =) name testers, genctxt)
- else
- error ("Unknown tester: " ^ name);
+ else error ("Unknown tester: " ^ name);
fun parse_test_param ("tester", args) = fold parse_tester args
| parse_test_param ("size", [arg]) = apsnd (Config.put_generic size (read_nat arg))
| parse_test_param ("iterations", [arg]) = apsnd (Config.put_generic iterations (read_nat arg))
| parse_test_param ("depth", [arg]) = apsnd (Config.put_generic depth (read_nat arg))
- | parse_test_param ("default_type", arg) = (fn (testers, gen_ctxt) =>
- (testers, map_test_params
- ((apfst o K) (map (Proof_Context.read_typ (Context.proof_of gen_ctxt)) arg)) gen_ctxt))
+ | parse_test_param ("default_type", arg) =
+ (fn (testers, context) =>
+ (testers, map_test_params
+ (apfst (K (map (Proof_Context.read_typ (Context.proof_of context)) arg))) context))
| parse_test_param ("no_assms", [arg]) = apsnd (Config.put_generic no_assms (read_bool arg))
- | parse_test_param ("expect", [arg]) = apsnd (map_test_params ((apsnd o K) (read_expectation arg)))
+ | parse_test_param ("expect", [arg]) = apsnd (map_test_params (apsnd (K (read_expectation arg))))
| parse_test_param ("report", [arg]) = apsnd (Config.put_generic report (read_bool arg))
- | parse_test_param ("genuine_only", [arg]) = apsnd (Config.put_generic genuine_only (read_bool arg))
- | parse_test_param ("abort_potential", [arg]) = apsnd (Config.put_generic abort_potential (read_bool arg))
+ | parse_test_param ("genuine_only", [arg]) =
+ apsnd (Config.put_generic genuine_only (read_bool arg))
+ | parse_test_param ("abort_potential", [arg]) =
+ apsnd (Config.put_generic abort_potential (read_bool arg))
| parse_test_param ("quiet", [arg]) = apsnd (Config.put_generic quiet (read_bool arg))
| parse_test_param ("verbose", [arg]) = apsnd (Config.put_generic verbose (read_bool arg))
| parse_test_param ("tag", [arg]) = apsnd (Config.put_generic tag arg)
- | parse_test_param ("use_subtype", [arg]) = apsnd (Config.put_generic use_subtype (read_bool arg))
- | parse_test_param ("timeout", [arg]) = apsnd (Config.put_generic timeout (read_real arg))
- | parse_test_param ("finite_types", [arg]) = apsnd (Config.put_generic finite_types (read_bool arg))
+ | parse_test_param ("use_subtype", [arg]) =
+ apsnd (Config.put_generic use_subtype (read_bool arg))
+ | parse_test_param ("timeout", [arg]) =
+ apsnd (Config.put_generic timeout (read_real arg))
+ | parse_test_param ("finite_types", [arg]) =
+ apsnd (Config.put_generic finite_types (read_bool arg))
| parse_test_param ("allow_function_inversion", [arg]) =
apsnd (Config.put_generic allow_function_inversion (read_bool arg))
| parse_test_param ("finite_type_size", [arg]) =
- apsnd (Config.put_generic finite_type_size (read_nat arg))
+ apsnd (Config.put_generic finite_type_size (read_nat arg))
| parse_test_param (name, _) =
(fn (testers, genctxt) =>
if valid_tester_name genctxt name then
(insert (op =) name testers, genctxt)
else error ("Unknown tester or test parameter: " ^ name));
-fun proof_map_result f = apsnd Context.the_proof o f o Context.Proof;
-
fun parse_test_param_inst (name, arg) ((insts, eval_terms), (testers, ctxt)) =
(case try (Proof_Context.read_typ ctxt) name of
SOME (TFree (v, _)) =>
@@ -485,10 +498,14 @@
"eval" => ((insts, eval_terms @ map (Syntax.read_term ctxt) arg), (testers, ctxt))
| _ =>
((insts, eval_terms),
- proof_map_result (fn gen_ctxt => parse_test_param (name, arg) (testers, gen_ctxt)) ctxt)));
+ let
+ val (testers', Context.Proof ctxt') =
+ parse_test_param (name, arg) (testers, Context.Proof ctxt);
+ in (testers', ctxt') end)));
-fun quickcheck_params_cmd args = Context.theory_map
- (fn gen_ctxt => uncurry set_active_testers (fold parse_test_param args ([], gen_ctxt)));
+fun quickcheck_params_cmd args =
+ Context.theory_map
+ (fn context => uncurry set_active_testers (fold parse_test_param args ([], context)));
fun check_expectation state results =
if is_some results andalso expect (Proof.context_of state) = No_Counterexample then
@@ -502,8 +519,10 @@
|> Proof.map_context_result (fn ctxt =>
apsnd (fn (testers, ctxt) => Context.proof_map (set_active_testers testers) ctxt)
(fold parse_test_param_inst args (([], []), ([], ctxt))))
- |> (fn ((insts, eval_terms), state') => test_goal (true, true) (insts, eval_terms) i state'
- |> tap (check_expectation state') |> rpair state');
+ |> (fn ((insts, eval_terms), state') =>
+ test_goal (true, true) (insts, eval_terms) i state'
+ |> tap (check_expectation state')
+ |> rpair state');
fun quickcheck args i state =
Option.map (the o get_first counterexample_of) (fst (gen_quickcheck args i state));
