overture
overture copied to clipboard
overturetool
HTML Export of Specifications
Overture has a feature that generates a LaTeX/PDF copy of a project. The output is fine as far as it goes, but it is static and while good for reading a specification top-to-bottom, it is less so for trying to understand a specification, a process that inevitably entails much jumping around.
Hyperlinking as is commonly used in browsers would allow much more dynamic viewing of specifications, enabling one to drill down through function and type definitions, and ascend back up the search tree. A simple example of this can be found in the set of attached VDM-SL specifications. Clicking on a type or function definition navigates to that definition, including jumping to a definition in a different module, and the browser 'Back' button allows one to return to previous selections.
It would be very useful if Overture was able to generate a set of HTML files from a project in a similar manner. The dynamic nature of the output greatly facilitates the process of reading/reviewing/understanding specifications, and would not require an Overture installation.
Other possibilities are open. For example, a tree structure reflecting the hierarchy of the modules could also be provided, similar to the VDM Explorer pane in Overture, or the frames version of the Java Platform API documentation.
I like this idea. I don't know the current status of Overture Web IDE, but If Overture Web IDE has such Web API, we can construct a evaluatable documentation of VDM specs.
For VDM-SL, VDMPad (http://vdmpad.csce.kyushu-u.ac.jp/) has a Web API that evaluates the given expression with the given specification and the given state.
For example, http://vdmpad.csce.kyushu-u.ac.jp/eval?source=functions%20inc:nat-%3Enat%20inc(x)==x%2b1;&expression=inc(2) evaluates inc(2) given the spec
functions
inc : nat -> nat
inc(x) == x + 1;
I think the combination of HTML-ization and Web IDE looks very attractive to me.
As a very simple example of an explorer capability, the attached adds two files. View 'frame.html' in a browser as the starting point.
Is there any way we can use this technology to improve the "definition location" functionality of the Overture VDM Editor? Currently, if you sit on (say) a mk_R expression or a function call and press F3, the editor takes you to the definition of R or the function - just like the Java Editor does in Eclipse.
This is a very useful feature for large specifications, but unfortunately the current implementation is very buggy - F3 may not jump anywhere, or may jump to the wrong location. I was wondering whether Paul's idea might be the basis of a way to improve this, since the HTML output effectively does the hyperlinking for you, but of course outside the editor currently.
These seem like 2 different features to me.
Linking definitions to names is AST links and lookups. I don't know if the bugs in the current feature stem from broken AST links, but I suspect they do not since the interpreter can find definitions correctly. My guess is that the cursor position isn't always picked up correctly (there are also some issues with lex locations).
The HTML generation is a more sophisticated pretty-printing, though it would of course use links existing in the AST. Assuming those are correct, I do not see this as a difficult task, but it would be quite lengthy, considering the size of the AST.
Yes, I agree they are different things. But I was wondering whether the technology from the new parse could be used to fix the editor. I vaguely remember that the editor does its own parse, every time you pause for a second or two after typing something, and that is independent of the parse that happens when a type check is performed? If that's true, it may be easy to drop different parser technology into the editor.
I'm just guessing to be honest, but it seemed like an opportunity because the "F3" lookups are definitely useful and definitely broken!
I'm not sure what you mean by "new parse".
As far as I understand/remember..
- the parse-as-you-type is an Eclipse hook and we call the Overture parser from there.
- I'm not aware of there being a separate parser used only by the editor, but I could be wrong.
- Parse-as-you-type has never worked very well (it's extremely easy to break it in normal use).
- The type checker is only invoked when we save. This invocation is preceded by a call to the parser.
Completely agree on the F3 lookups. I think a pair of students built the first version. @peterwvj can you confirm? Maybe they documented what's missing?
By "new parse" I mean Paul's ANTLR parser. So instead of the editor hook calling out to the Overture parser, perhaps it could call ANTLR derived parser that returns hyperlink information that the editor can then use to implement "F3" jumps. It's probably not sensible... just throwing out ideas :)
It was @lausdahl who implemented the first version of the "go-to-declaration" feature. I don't think the students had anything to do with it. The students developed the auto-completion feature (which is included in the tool) and simple refactoring support (which is not yet included in the tool).
The "go-to-declaration" feature uses the visitor-based AstLocationSearcher* classes to look up declarations. I can't remember exactly why this feature sometimes fails to find the corresponding declarations. It could be caused by missing visitor cases, but I vaguely recall Kenneth saying something about the position information sometimes being inaccurate. I'm guessing it's a mix of both.
Right now, the AstLocationSearcher* classes are contained in one of the IDE projects, which makes it difficult to automate testing of this feature. As a first step these classes should be moved to a core module.
Issue #608 covers the F3 bug. I'm sorry if I caused Paul's idea and the F3 problem to get entangled when they are not directly related. I'll add a reference to this issue from #608.
Since we are on the topic of F3. One of the nice things about browsing in HTML is the ease with which you can return to what you were viewing previously, with the 'Back' button. Is there anything like that in Overture, or the Eclipse framework that could be used for the purpose?
Eclipse (and Overture) have left/right "arrow icons" that you can hopefully see on the tool bar? Or you can use Alt-Left and Alt-Right arrow. The options are also available in the Navigate menu. They basically remember the last few locations, and will return from an F3.