[isabelle-dev] Notes on Isabelle/Scala systems programming

[Makarius]

On Tue, 29 Apr 2014, Makarius wrote:

> I've just done again to update all Isabelle + AFP ROOT files, using standard 
> Isabelle functions that are already there, but also adding a few more bits 
> like Isabelle_System.hg for Mercurial command line tools.

Maybe this needs an example how it works (on the Scala console):

   import isabelle._

   val afp_base = Path.explode("$AFP_BASE")
   val afp_files = Isabelle_System.hg("manifest", afp_base).check_error.out_lines

Now we can operate systematically on the real AFP files, not the junk that 
happens to lie around in the file-system.  E.g. like this:

   for { a <- afp_files; if a.endsWith(".thy") || a.endsWith(".ML") } Check_Source.check_file(afp_base + Path.explode(a))

Normally I don't write such exceedingly long source lines, but the Scala 
console might need just one line to copy-paste.


 	Makarius