TWiki> PG Web>PGIPIdeasForPML (revision 1)EditAttach

Notes on PGIP support for PML

-- DavidAspinall - 19 Jun 2007

Use cases for PML


  • showing syntax and typing errors
  • editing of a hole
    • editing the whole file will require re-parsing whole file
    • to start with, we probably will typecheck whole file every time
    • in step 2, we may think of optimising for editing a whole
    • in step 3, think about undo for replacing text
  • undo or putting back a hole
  • querying the context

Type-check file

  1. -> PML: type-check a whole file (sent as a string)
  2. <- Something naming holes and/or error messages


  • Holes are just comments, can contain any text (not checked)
  • Do we want user-level names for holes? We certainly need system-level names (e.g., numbers)
  • Probably there is no concrete syntax in PML for hole names!

Idea for system-level hole identifiers:

But: these are then changed by edits, which might be bad. Alternative is to use goal numbers constructed for tree path, but paths get long quickly. PhoX uses some relative scheme for goal numbers which helps avoid this problem.

For interface access without clicking, we do want these numbers to be usable.

Solution: use both! <X,Y> with X the history number, Y the index of the goal as it appears in the file.

Displaying errors

  • PML produces three positions for an error, would like to distinguish these by colour
  • These are: position of error, then position of match, position of variant itself
  • Underlying graph of type system actually gives some dataflow, would be nice to display this in the interface (even animate it somehow)
  • Possible solution: use PGML markup for adding highlighting?
  • At the moment, PML only returns one error, this can be displayed using three markers in Eclipse with the same (or, related) error message
  • These could maybe be flagged with infos/warnings

[ Aside: in Proof General, students first assume that after an error they must do undo! This is wrong! ]


  • Q. How does indentation work? A. by adding the and elements,
which can be used by the interface to optionally indent the code (like TAB in Emacs).


  • Agda-style interaction: proof construction occurs by writing proof terms by filling holes
Edit | Attach | Print version | History: r2 < r1 | Backlinks | Raw View | Raw edit | More topic actions...
Topic revision: r1 - 19 Jun 2007 - 10:01:29 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies