Here are some further refinements leading up to Isabelle/3a6c03b15916.
* The "Session Modelling Language" (S.M.L.) has been simplified to
accomodate applications better, instead of the received layout of the
Isabelle distribution.
Session names are always verbatim (without implicit concatenation) and
the default directory is "." (not the session base name).
Examples from the distribution:
session HOL = Pure + theories Complex_Main
session "HOL-Nominal" in Nominal = HOL + theories Nominal
session "HOL-Nominal-Examples" in "Nominal/Examples" = "HOL-Nominal" +
theories Nominal_Examples
theories [quick_and_dirty] VC_Condition
Examples from AFP:
session "Depth-First-Search" (AFP) = HOL +
theories DFS
session BDD (AFP) = Simpl +
theories
EvalProof
NormalizeTotalProof
files
"document/root.bib"
"document/root.tex"
* "isabelle build -D DIR" includes a directory and selects all its
session defined there.
* "isabelle mkroot" has been refined a bit. I still need to figure out
how to avoid "document_dump" in most practical situations. (It is not
enabled there now.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
