[isabelle-dev] NEWS: activation of Z3 via "z3_non_commercial" system option

[Makarius]

* Activation of Z3 now works via "z3_non_commercial" system option
(without requiring restart), instead of former settings variable
"Z3_NON_COMMERCIAL".  The option can be edited in Isabelle/jEdit menu
Plugin Options / Isabelle / General.

This refers to Isabelle/0c07990363a3.  For completeness, the included diff 
shows the update on the Isabelle component z3-3.2-1, which is relevant for 
Jasmin when he changes z3 again in the future.

The change of z3_non_commercial was already planned for Isabelle2013-2, 
but did not make it into the release, because I could not make up my mind 
how much hand-holding the user should get.  Right now it is the minimal 
possible approach to it, without any hand-holding apart from some prose 
text.

I have taken the opportunity to experiment with Pretty.para here: 
traditionally we have short one-line output that is statically broken, but 
here the long text might look better with dynamic word-wrapping.  The 
disadvantage is that such output is harder to search formally in log files 
etc.


 	Makarius
-------------- next part --------------
diff -r z3-3.2/etc/settings z3-3.2-1/etc/settings
4,6c4
< Z3_HOME="$Z3_COMPONENT/$ISABELLE_PLATFORM"
< 
< # Z3_NON_COMMERCIAL="yes"
---
> Z3_HOME="$Z3_COMPONENT/$ISABELLE_PLATFORM32"
Only in z3-3.2/etc: ._settings
diff -r z3-3.2/README z3-3.2-1/README
16,19c16,17
< 
<     Z3_NON_COMMERCIAL="yes"
< 
< in the environment or in "$ISABELLE_HOME_USER/etc/settings".
---
> the Isabelle system option "z3_non_commercial" to "yes" (e.g. via the
> Isabelle/jEdit menu Plugin Options / Isabelle / General).
Only in z3-3.2/x86-darwin: z3.dbg