[isabelle-dev] build and run Isabelle/jEdit on the spot

[Christian Sternagel]

Hi,

for me this fails with the attached errors. Any ideas? -cheers chris

###
### Building Isabelle/Scala layer ...
###
General/xml.scala:153: error: value err is not a member of package System
           case bad => System.err.println("XML.cache_actor: ignoring bad 
input " + bad)
                              ^
PIDE/command.scala:45: error: value err is not a member of package System
               case _ => System.err.println("Ignored status message: " + 
msg); state
                                ^
PIDE/command.scala:73: error: value err is not a member of package System
             case _ => System.err.println("Ignored message without 
serial number: " + message); this
                              ^
PIDE/document.scala:315: error: value err is not a member of package System
               System.err.println((true, range, edits)); throw(e)
                      ^
PIDE/document.scala:322: error: value err is not a member of package System
               System.err.println((false, range, reverse_edits)); throw(e)
                      ^
PIDE/markup_tree.scala:84: error: value err is not a member of package 
System
             System.err.println("Ignored overlapping markup information: 
" + new_info)
                    ^
System/event_bus.scala:23: warning: abstract type Event in type pattern 
Event is unchecked since it is eliminated by erasure
     this += actor { loop { react { case x: Event => f(x) } } }
                                            ^
System/platform.scala:19: error: value getProperty is not a member of 
package System
   val is_windows = System.getProperty("os.name").startsWith("Windows")
                           ^
System/gui_setup.scala:59: error: value exit is not a member of package 
System
       case ButtonClicked(`ok`) => System.exit(0)
                                          ^
System/isabelle_process.scala:144: error: value currentTimeMillis is not 
a member of package System
       val expired = System.currentTimeMillis() + timeout.ms
                            ^
System/isabelle_process.scala:148: error: value currentTimeMillis is not 
a member of package System
       while (finished.isEmpty && System.currentTimeMillis() <= expired) {
                                         ^
System/isabelle_process.scala:226: error: value err is not a member of 
package System
             case bad => System.err.println(name + ": ignoring bad 
message " + bad)
                                ^
System/isabelle_process.scala:293: error: value err is not a member of 
package System
             case bad => System.err.println(name + ": ignoring bad 
message " + bad)
                                ^
System/platform.scala:18: error: value getProperty is not a member of 
package System
   val is_macos = System.getProperty("os.name") == "Mac OS X"
                         ^
System/session.scala:83: error: value currentTimeMillis is not a member 
of package System
         case Some(time) => (time - System.currentTimeMillis()) max 0
                                           ^
System/session.scala:95: error: value currentTimeMillis is not a member 
of package System
       val now = System.currentTimeMillis()
                        ^
System/session.scala:108: error: value err is not a member of package System
         case bad => System.err.println("command_change_buffer: ignoring 
bad message " + bad)
                            ^
System/session.scala:194: error: value err is not a member of package System
         System.err.println("Ignoring prover result: " + 
result.message.toString)
                ^
System/session.scala:283: error: value err is not a member of package System
           System.err.println("session_actor: ignoring bad message " + bad)
                  ^
System/standard_system.scala:315: error: value getProperty is not a 
member of package System
     val java_home = System.getProperty("java.home")
                            ^
one warning found
19 errors found
Failed to compile sources

On 05/21/2011 09:41 PM, Alexander Krauss wrote:
> On 05/21/2011 12:55 AM, Makarius wrote:
>> In Isabelle/4a26abd3d57b Isabelle/jEdit can be built and run on the spot
>> as follows:
>>
>> * Deactivate any existing jedit component setup in
>> $ISABELLE_HOME_USER/etc/settings or
>> $ISABELLE_HOME_USER/etc/components etc.
>>
>> * Make sure that SCALA_HOME within the Isabelle environment points to
>> scala-2.8.1.final (Isabelle2011 ships that version as component
>> which can be re-used here).
>>
>> * Download and unpack
>> http://www4.in.tum.de/~wenzelm/test/jedit_build-20110521.tar.gz
>>
>> This contains all external jars required to build Isabelle/jEdit from
>> source. It needs to be initialized as component as usual, e.g. like
>> this in "$ISABELLE_HOME_USER/etc/settings":
>>
>> init_component "$HOME/isabelle/jedit_build-20110521"
>
> I initially had some build problems, which I post here in case other
> people experience the same:
>
> * It was important that scala-2.8.1.final is initialized before
> jedit_build-20110521. I initially got this wrong, which resulted in a
> broken build.
>
> * Fixing the situation involved swapping the respective lines in my
> ~/.isabelle/etc/components, and ensuring that everything is really built
> from scratch. In particular, I had to
>
> - remove the jars from $ISABELLE_HOME/lib/classes
> - remove the jedit-4.3.2... directory from the jedit_build component
> directory.
>
>> Now enjoy blue/green/brown variables and hyperlinks for most formal
>> entities in the source text.
>
> Sweet!
>
> Alex
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>