On 19/01/2024 14:45, Andrew Goh via polyml wrote:
As the latest Poly/ML 5.9.1 version is not available for Windows, I however managed to obtain a previous version 5.5.0 from source forge.
I was wondering if Poly/ML can be improved until it looks like, feels like and works like a copy of the Python IDLE IDE.
I know very little about Python and have never seen IDLE before, but here is a quite different document-oriented IDE for many languages, including Isabelle/ML (based on Poly/ML): https://isabelle.in.tum.de
That should also work on Windows out-of-the-box.
Within the IDE, the "Documentation" panel on the left has some "Examples", notably:
src/HOL/Examples/ML.thy src/Tools/SML/Examples.thy
These are formal documents that contain explanations in prose, definitions in the formal languages, and expressions that you can evaluate on the spot (while editing). There is no separate "shell" window.
Isabelle/ML is mainly for mathematical programming in a purely functional environment. Thus you evaluate expressions on the spot during the editing process: deleting an expression will stop its evaluation and remove its result from the document. This model won't work as expected, if you cause effects on the surrounding physical world (like writing files).
The proper language for physics (not mathematics) in the Isabelle universe is Isabelle/Scala: it has a Console window, but is not covered by the IDE.
Makarius