On 25 Sep 2013, at 12:00, Makarius <makar...@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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev