Hi all,
I'd like to report two problems with Isabelle (b17b05c8d4a4) -- AFP
(40ecbad14077).
1. In Proof General:
theory Scratch
imports
"$MY_AFP_DEVEL_HOME/thys/Jinja/J/TypeSafe"
"~~/src/HOL/Proofs/Lambda/StrongNorm"
begin
nondeterministically gives either
*** Undeclared type constructor: "vname" (line 12 of
"/Users/blanchet/afp/thys/Jinja/Common/Decl.thy")
*** Failed to parse type
*** in type abbreviation "fdecl"
*** At command "type_synonym" (line 11 of
"/Users/blanchet/afp/thys/Jinja/Common/Decl.thy")
or
*** Inner lexical error at: ⟪i:U⟫ ⊢ t : T ⟹
*** IT u ⟹ e ⊢ u : U ⟹ IT (t[u/i]) (line 91 of
"~~/src/HOL/Proofs/Lambda/StrongNorm.thy")
*** Failed to parse proposition
*** At command "lemma" (line 90 of
"~~/src/HOL/Proofs/Lambda/StrongNorm.thy")
but each of them loads fine on its own.
2. I then wanted to try in jEdit but "isabelle jedit" gives this error:
### Building Isabelle/jEdit ...
src/graphview_dockable.scala:45: error: object graphview is not a member of
package isabelle
new
isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
^
src/graphview_dockable.scala:45: error: too many arguments for constructor
Object: ()java.lang.Object
new
isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
^
src/graphview_dockable.scala:53: error: value peer is not a member of
AnyRef{def make_tooltip(parent: javax.swing.JComponent,x: Int,y: Int,body:
isabelle.XML.Body): String}
graphview.add(panel.peer, BorderLayout.CENTER)
^
three errors found
Failed to compile sources
From what I recall, "isabelle jedit" worked fine on my machine (Mac OS X 10.6)
just one or two weeks ago.
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
