# HG changeset patch # User wenzelm # Date 1392929108 -3600 # Node ID 79a43f8e18a3498d97937574e801f557f94f34b8 # Parent 9066b603dff6c0c331e93ff73973b3fd0c6aa4ca# Parent 9d120886c50b0afcb9487fd7d15d5c1f23a2c516 merged diff -r 9066b603dff6 -r 79a43f8e18a3 NEWS --- 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: diff -r 9066b603dff6 -r 79a43f8e18a3 src/HOL/HOL.thy --- 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 *} diff -r 9066b603dff6 -r 79a43f8e18a3 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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. *) diff -r 9066b603dff6 -r 79a43f8e18a3 src/HOL/Tools/Nitpick/nitpick_scope.ML --- 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) = diff -r 9066b603dff6 -r 79a43f8e18a3 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- 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)) diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/GUI/swing_thread.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/General/antiquote.ML --- 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; diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/General/bytes.scala --- 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) } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/General/linear_set.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/General/multi_map.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/General/position.ML --- 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 "\\" 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 ("", "\\") 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; diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/General/symbol.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/General/timing.scala --- 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") diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Isar/completion.scala --- 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))) diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Isar/outer_syntax.scala --- 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) + } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Isar/parse.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/ML/ml_antiquote.ML --- 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") #> diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/ML/ml_lex.ML --- 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; diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/PIDE/command.scala --- 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 } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/PIDE/document.scala --- 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) } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/PIDE/markup.ML --- 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 *) diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/PIDE/markup.scala --- 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 */ diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/PIDE/markup_tree.scala --- 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) diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/PIDE/query_operation.scala --- 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) } } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/PIDE/xml.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Syntax/lexicon.ML --- 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; diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Syntax/parser.ML --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/System/command_line.scala --- 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) diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/System/event_bus.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/System/isabelle_charset.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/System/isabelle_font.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/System/isabelle_process.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/System/isabelle_system.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/System/options.scala --- 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)) diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/System/platform.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/System/session.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Thy/html.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Thy/thy_load.ML --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Thy/thy_output.ML --- 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; diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Tools/build.scala --- 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) } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Tools/keywords.scala --- 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) } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Tools/main.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Tools/rail.ML --- 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; diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/Tools/simplifier_trace.ML --- 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" diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/display.ML --- 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 [] diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/more_thm.ML --- 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); diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/raw_simplifier.ML --- 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 $ _ => diff -r 9066b603dff6 -r 79a43f8e18a3 src/Pure/variable.ML --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/Graphview/src/graph_panel.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/Graphview/src/model.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/Graphview/src/mutator_dialog.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/Graphview/src/popups.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/Graphview/src/visualizer.scala --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/coherent.ML --- 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; diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/cong_tac.ML --- 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); diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/intuitionistic.ML --- 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 diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/PIDE.png Binary file src/Tools/jEdit/PIDE.png has changed diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/completion_popup.scala --- 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 = diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/document_view.scala --- 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) } } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/find_dockable.scala --- 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) } } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/info_dockable.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/isabelle.scala --- 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 } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/monitor_dockable.scala --- 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) } } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/output_dockable.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/plugin.scala --- 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) } } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/protocol_dockable.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/raw_output_dockable.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/rendering.scala --- 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) }) } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/scala_console.scala --- 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) diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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) } } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/syslog_dockable.scala --- 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) } } } diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/theories_dockable.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/jEdit/src/timing_dockable.scala --- 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} diff -r 9066b603dff6 -r 79a43f8e18a3 src/Tools/quickcheck.ML --- 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));