[isabelle-dev] sledgehammer panel problem
Lawrence Paulson
lp15 at cam.ac.uk
Wed Sep 25 15:20:54 CEST 2013
On 25 Sep 2013, at 12:00, Makarius <makarius at sketis.net> wrote:
> Now I understand what you mean. I've addresses this here:
>
> changeset: 53867:6e69f9ca8f1c
> user: wenzelm
> date: Wed Sep 25 11:12:59 2013 +0200
> files: src/Pure/PIDE/query_operation.scala src/Tools/jEdit/src/find_dockable.scala src/Tools/jEdit/src/sledgehammer_dockable.scala
> description:
> explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d);
That's great news, thanks!
Unfortunately, I seem to be having problems with this version (f54a8f591e0f).
I tried the usual tricks but I still get compilation errors.
Larry
~/isabelle/hfinite/Incompleteness: isabelle jedit -f SyntaxN.thy
### Building Isabelle/Scala ...
GUI/gui.scala:47: error: not found: value split_lines
if (height > 0 && split_lines(txt).length > height) text.rows = height
^
GUI/gui.scala:118: error: not found: value cat_lines
else "<html><pre>" + HTML.encode(cat_lines(lines)) + "</pre></html>"
^
GUI/system_dialog.scala:64: error: not found: value ERROR
catch { case ERROR(_) => }
^
PIDE/yxml.scala:55: error: not found: value quote
else err("unbalanced element " + quote(name))
^
PIDE/yxml.scala:128: error: not found: value ERROR
catch { case ERROR(_) => List(markup_broken(source)) }
^
PIDE/yxml.scala:134: error: not found: value ERROR
catch { case ERROR(_) => markup_broken(source) }
^
General/file.scala:140: error: not found: value ERROR
catch { case ERROR(_) => false }
^
General/path.scala:27: error: not found: value quote
error(msg + " path element specification " + quote(s))
^
General/path.scala:34: error: not found: value quote
err_elem("Illegal character " + quote(c.toString) + " in", s))
^
General/path.scala:85: error: not found: value ERROR
catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) }
^
General/path.scala:85: error: not found: value cat_error
catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) }
^
General/path.scala:87: error: not found: value space_explode
val ss = space_explode('/', str)
^
General/path.scala:95: error: value filterNot is not a member of Any
val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
^
General/path.scala:101: error: not found: value ERROR
try { explode(str); true } catch { case ERROR(_) => false }
^
General/path.scala:104: error: not found: value space_explode
space_explode(':', str).filterNot(_.isEmpty).map(explode)
^
General/path.scala:131: error: not found: value quote
override def toString: String = quote(implode)
^
General/position.scala:95: error: not found: value quote
case (Some(i), Some(name)) => " (line " + i.toString + " of " + quote(name) + ")"
^
General/position.scala:96: error: not found: value quote
case (None, Some(name)) => " (file " + quote(name) + ")"
^
General/pretty.scala:89: error: not found: value split_lines
case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
^
General/symbol.scala:180: error: not found: value quote
error("Duplicate mapping of " + quote(x) + " to " + quote(y) + " vs. " + quote(z))
^
General/symbol.scala:241: error: not found: value split_lines
split_lines(symbols_spec).reverse)
^
General/symbol.scala:405: error: not found: value commas_quote
error("Bad Unicode symbols in text: " + commas_quote(bad))
^
Isar/completion.scala:56: error: not found: value ERROR
case ERROR(msg) => ignore_error(msg); Nil
^
Isar/completion.scala:56: error: not found: value msg
case ERROR(msg) => ignore_error(msg); Nil
^
Isar/outer_syntax.scala:50: error: not found: value quote
if (kind == Keyword.MINOR) quote(name)
^
Isar/parse.scala:51: error: not found: value quote
atom("command " + quote(name), tok => tok.is_command && tok.source == name)
^
Isar/parse.scala:54: error: not found: value quote
atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
^
Isar/token.scala:44: error: not found: value quote
else ("line " + line.toString + " of " + quote(file))
^
PIDE/protocol.scala:23: error: not found: value ERROR
case ERROR(_) => None
^
PIDE/protocol.scala:36: error: not found: value ERROR
case ERROR(_) => None
^
System/invoke_scala.scala:28: error: not found: value quote
error("No such method: " + quote(name))
^
System/invoke_scala.scala:40: error: not found: value quote
case _ => error("Malformed method name: " + quote(name))
^
System/invoke_scala.scala:97: error: not found: value default_thread_pool
default_thread_pool.submit(() =>
^
System/isabelle_system.scala:155: error: not found: value space_explode
for (p <- space_explode('/', rest) if p != "") {
^
System/isabelle_system.scala:224: error: not found: value quote
if (!path.is_dir) error("Cannot create directory: " + quote(platform_path(path)))
^
System/isabelle_system.scala:353: error: not found: value cat_lines
def out: String = cat_lines(out_lines)
^
System/isabelle_system.scala:354: error: not found: value cat_lines
def err: String = cat_lines(err_lines)
^
System/options.scala:39: error: not found: value quote
(if (typ == Options.String) quote(x) else x) +
^
System/options.scala:48: error: not found: value space_explode
val words = space_explode('_', name)
^
System/options.scala:54: error: type mismatch;
found : String => String
required: Any => ?
words1.map(Library.capitalize).mkString(" ")
^
System/options.scala:111: error: not found: value ERROR
catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
^
System/options.scala:111: error: not found: value msg
catch { case ERROR(msg) => error(msg + Position.here(file.position)) }
^
System/options.scala:152: error: not found: value cat_lines
case _ => error("Bad arguments:\n" + cat_lines(args))
^
System/options.scala:165: error: not found: value cat_lines
def print: String = cat_lines(options.toList.sortBy(_._1).map(p => p._2.print))
^
System/options.scala:175: error: not found: value quote
case _ => error("Unknown option " + quote(name))
^
System/options.scala:182: error: not found: value quote
else error("Ill-typed option " + quote(name) + " : " + opt.typ.print + " vs. " + typ.print)
^
System/options.scala:200: error: not found: value quote
error("Malformed value for option " + quote(name) +
^
System/options.scala:264: error: not found: value quote
case Some(_) => error("Duplicate declaration of option " + quote(name))
^
System/options.scala:272: error: not found: value quote
case _ => error("Unknown type for option " + quote(name) + " : " + quote(typ_name))
^
System/options.scala:300: error: not found: value quote
case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
^
System/session.scala:77: error: not found: value commas_quote
if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
^
System/session.scala:98: error: not found: value quote
quote(a) + "\n" + Exn.message(exn))
^
System/session.scala:202: error: not found: value cat_lines
def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
^
System/session.scala:242: error: not found: value quote
header.error("Attempt to update loaded theory " + quote(name.theory))
^
Thy/thy_header.scala:36: error: not found: value quote
s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
^
Thy/thy_info.scala:18: error: not found: value quote
names.map(name => quote(name.theory)).mkString(" via ")
^
Thy/thy_info.scala:90: error: not found: value cat_error
cat_error(msg, "The error(s) above occurred while examining theory " +
^
Thy/thy_info.scala:97: error: not found: value ERROR
catch { case ERROR(msg) => err(msg) }
^
Thy/thy_info.scala:97: error: not found: value msg
catch { case ERROR(msg) => err(msg) }
^
Thy/thy_load.scala:23: error: not found: value ERROR
catch { case ERROR(_) => false }
^
Thy/thy_load.scala:114: error: not found: value quote
" for theory " + quote(name1))
^
Tools/build.scala:104: error: not found: value ERROR
case ERROR(msg) =>
^
Tools/build.scala:105: error: not found: value msg
error(msg + "\nThe error(s) above occurred in session entry " +
^
Tools/build.scala:120: error: not found: value quote
error("Duplicate session " + quote(name) + Position.here(info.pos))
^
Tools/build.scala:130: error: not found: value quote
error("Bad parent session " + quote(parent) + " for " +
^
Tools/build.scala:136: error: not found: value cat_lines
error(cat_lines(exn.cycles.map(cycle =>
^
Tools/build.scala:157: error: not found: value commas_quote
if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
^
Tools/build.scala:289: error: not found: value split_lines
line <- split_lines(File.read(roots))
^
Tools/build.scala:445: error: not found: value cat_lines
progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _)))
^
Tools/build.scala:630: error: not found: value split_lines
val lines = split_lines(text)
^
Tools/build.scala:753: error: not found: value ERROR
case ERROR(msg) => ignore_error(msg)
^
Tools/build.scala:753: error: not found: value msg
case ERROR(msg) => ignore_error(msg)
^
Tools/build.scala:820: error: not found: value cat_lines
progress.echo("\n" + cat_lines(tail))
^
Tools/build.scala:953: error: not found: value commas
progress.echo("Unfinished session(s): " + commas(unfinished))
^
Tools/build.scala:986: error: not found: value cat_lines
case _ => error("Bad arguments:\n" + cat_lines(args))
^
Tools/doc.scala:30: error: not found: value split_lines
line <- split_lines(Library.trim_line(File.read(catalog)))
^
Tools/doc.scala:87: error: not found: value quote
"\"$ISABELLE_TOOL\" display " + quote(doc) + " >/dev/null 2>/dev/null &")
^
Tools/doc.scala:88: error: not found: value quote
case None => error("Missing Isabelle documentation file: " + quote(doc))
^
Tools/doc.scala:98: error: not found: value cat_lines
if (args.isEmpty) Console.println(cat_lines(contents_lines()))
^
Tools/keywords.scala:107: error: not found: value quote
error("Inconsistent declaration of keyword " + quote(name) + ": " +
^
Tools/keywords.scala:134: error: not found: value quote
names.map(name => quote("""[\.\*\+\?\[\]\^\$]""".r replaceAllIn (name, """\\\\$0""")))
^
Tools/keywords.scala:176: error: not found: value cat_lines
case _ => error("Bad arguments:\n" + cat_lines(args))
^
Tools/main.scala:140: error: not found: value quote
error("Bad Isabelle home directory: " + quote(isabelle_home))
^
83 errors found
Failed to compile sources
~/isabelle/hfinite/Incompleteness: hg id
f54a8f591e0f tip
More information about the isabelle-dev
mailing list