Maybe Florian also has some ideas about codegen.
One answer would be to eliminate this meanwhile somehow ridiculous
warning entirely.
See now http://isabelle.in.tum.de/repos/isabelle/rev/e78c3023162b
Florian
--
PGP available:
On Mon, 29 Jul 2013, Florian Haftmann wrote:
Maybe Florian also has some ideas about codegen.
One answer would be to eliminate this meanwhile somehow ridiculous
warning entirely.
See now http://isabelle.in.tum.de/repos/isabelle/rev/e78c3023162b
Great.
In the meantime (leading up to the
Am 18/07/2013 22:44, schrieb Makarius:
On Thu, 18 Jul 2013, Florian Haftmann wrote:
Code generator: dropping subsumed code equation by Auto Quickcheck
I guess it would be the task the tools to omit such outbursts and not
globally on the IDE side?
In principle Context_Position.is_visible
On Fri, 19 Jul 2013, Tobias Nipkow wrote:
I have generalized the concept to allow changing the visibility of a
global theory context as well. This is observed by unify.ML, as a
guard to its many tracing options, find_theorems.ML then copies the
Proof.context visibility over to a copy of the
On Mon, 15 Jul 2013, Makarius wrote:
* Strictly monotonic document update, without premature cancelation of
running transactions that are still needed: avoid reset/restart of
such command executions while editing.
* Support for asynchronous print functions, as overlay to existing
document
Code generator: dropping subsumed code equation by Auto Quickcheck
I guess it would be the task the tools to omit such outbursts and not
globally on the IDE side?
In principle Context_Position.is_visible should control that, and the
tools should observe it accordingly.
The canonical way
On Thu, 18 Jul 2013, Florian Haftmann wrote:
Code generator: dropping subsumed code equation by Auto Quickcheck
I guess it would be the task the tools to omit such outbursts and not
globally on the IDE side?
In principle Context_Position.is_visible should control that, and the
tools should
On Thu, 18 Jul 2013, Makarius wrote:
On Thu, 18 Jul 2013, Florian Haftmann wrote:
Code generator: dropping subsumed code equation by Auto Quickcheck
I guess it would be the task the tools to omit such outbursts and not
globally on the IDE side?
In principle Context_Position.is_visible
On Mon, 15 Jul 2013, Makarius wrote:
On Mon, 15 Jul 2013, Dmitriy Traytel wrote:
Code generator: dropping subsumed code equation by Auto Quickcheck
I guess it would be the task the tools to omit such outbursts and not
globally on the IDE side?
In principle Context_Position.is_visible
* Strictly monotonic document update, without premature cancelation of
running transactions that are still needed: avoid reset/restart of
such command executions while editing.
* Support for asynchronous print functions, as overlay to existing
document content.
* Support for automatic tools in
10 matches
Mail list logo
