search

overturetool / overture

The Overture Tool
http://overturetool.org
GNU General Public License v3.0
48 stars 25 forks source link

Overture #ifdef processing does not work #710

Closed nickbattle closed 4 years ago

nickbattle commented 4 years ago

Both VDMJ and Overture (should!) have #ifdef functionality, which allows a section of a specification to be commented in or out, or alternatives to be selected, according to some properties. For example:

    f: nat -> nat
    #ifdef VDM_SL
    f(a) == a + 1;
    #else
    f(a) == a - 1;
    #endif

But this currently fails during the parse (Overture 2.7.2), being confused by the #else symbol.

The feature is generally useful, and we ought to fix this.

nickbattle commented 4 years ago

The problem was to do with the LatexStreamReader, which had been modified to work correctly with LaTeX suppression, but this had broken the #ifdef processing.

I've corrected this and, rather than just allowing the dialect names to be tested, the processing now checks for an arbitrary Java property as the #ifdef argument - and the three dialects set "VDM_SL", "VDM_PP" and "VDM_RT" as properties automatically. I also modified the keyword lists to include "#ifdef", "#else" and "#endif", so the editor shows these in a different colour.

Unfortunately, it is slightly inconvenient to set arbitrary properties in Overture/Eclipse. The only way I've found of making this work is (a) to update the Overture.ini file to set a global property, and (b) to use the "Debugger" field in a launch configuration to set a property for each runtime. NOTE that the runtime properties can be different to the editor therefore (which is confusing). The command line is very simple, as usual.

So this would need a little more work to be friendly, but the basic dialect-based #ifdef functionality is restored.

nickbattle commented 4 years ago

I just added and pushed a fix to allow #ifndef as well as #ifdef processing. That's sometimes more intuitive than using a #else clause.