[isabelle-dev] Two problems

[Jasmin Christian Blanchette]

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