Re: [isabelle-dev] sledgehammer panel problem
Sorry 7cec5a4d5532 Deleting Isabelle/lib/classes did the trick. Larry On 25 Sep 2013, at 14:58, Makarius wrote: > I don't see a public Isabelle version of that id -- isn't that your project > repository? > > Maybe your Isabelle clone got messed up locally, as a bad merge produced hy > "hg fetch" or "hg up". You can also try to purge Isabelle/lib/classes > carefully by hand. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
On Wed, 25 Sep 2013, Lawrence Paulson wrote:
I seem to be having problems with this version (f54a8f591e0f).
I tried the usual tricks but I still get compilation errors.
~/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
^
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
I don't see a public Isabelle version of that id -- isn't that your
project repository?
Maybe your Isabelle clone got messed up locally, as a bad merge produced
hy "hg fetch" or "hg up". You can also try to purge Isabelle/lib/classes
carefully by hand.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
On 25 Sep 2013, at 12:00, Makarius 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.encode(cat_lines(lines)) + ""
^
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
Re: [isabelle-dev] sledgehammer panel problem
On Tue, 24 Sep 2013, Lawrence Paulson wrote: my issue has nothing to do with editing the surrounding text. On the contrary, it has to do with activating s/h, walking away from the computer, and coming back to find that "sendback" does not work. 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); Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
Thanks for the response, but my issue has nothing to do with editing the surrounding text. On the contrary, it has to do with activating s/h, walking away from the computer, and coming back to find that "sendback" does not work. So I'm force to watch s/h and choose one of the metis calls before s/h terminates. Larry On 24 Sep 2013, at 20:52, Makarius wrote: > On Mon, 16 Sep 2013, Lawrence Paulson wrote: > >> Any generated "metis" calls only self-insert if clicked before s/h >> terminates. If you ignore your session for a few minutes while s/h runs (as >> many people do), then the highlighted links will be inactive when you get >> back. I've checked this several times. > > The "sendback" text addresses a particular command in the text, if that is > destroyed by editing, it will not work. > > Part of the problem is the old debate what a command span really is. 1.5 > years ago I've broken with ancient traditions and lessons learned from Proof > General and *included* trailing whitespace/comments here. This had a slight > advantage in the total number of command transactions. > > Many other surprises were coming from it, though. Here the snag is that > appending something after a command affects its trailing white space and thus > resets it. > > > In Isabelle/88c6e630c15f we are now back to the old scheme to *exclude* > trailing whitespace/comments and make a separate "ignored" command span > instead. The notion of "current_command" for Output and query operations > like Find or Sledgehammer is adapted accordingly. > > So the command where sledgehammer is applied is now more robust against edits > of the surrounding text. Hopefully this scheme is sufficient for this > release. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
On Mon, 16 Sep 2013, Lawrence Paulson wrote: Any generated "metis" calls only self-insert if clicked before s/h terminates. If you ignore your session for a few minutes while s/h runs (as many people do), then the highlighted links will be inactive when you get back. I've checked this several times. The "sendback" text addresses a particular command in the text, if that is destroyed by editing, it will not work. Part of the problem is the old debate what a command span really is. 1.5 years ago I've broken with ancient traditions and lessons learned from Proof General and *included* trailing whitespace/comments here. This had a slight advantage in the total number of command transactions. Many other surprises were coming from it, though. Here the snag is that appending something after a command affects its trailing white space and thus resets it. In Isabelle/88c6e630c15f we are now back to the old scheme to *exclude* trailing whitespace/comments and make a separate "ignored" command span instead. The notion of "current_command" for Output and query operations like Find or Sledgehammer is adapted accordingly. So the command where sledgehammer is applied is now more robust against edits of the surrounding text. Hopefully this scheme is sufficient for this release. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
~/isabelle/Repos/src/HOL: hg id 924579729403 tip Larry On 16 Sep 2013, at 12:25, Lawrence Paulson wrote: > Any generated "metis" calls only self-insert if clicked before s/h > terminates. If you ignore your session for a few minutes while s/h runs (as > many people do), then the highlighted links will be inactive when you get > back. I've checked this several times. > > Larry > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] sledgehammer panel problem
Any generated "metis" calls only self-insert if clicked before s/h terminates. If you ignore your session for a few minutes while s/h runs (as many people do), then the highlighted links will be inactive when you get back. I've checked this several times. Larry ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
