Opened 17 years ago

Closed 17 years ago

Last modified 11 years ago

#83 closed defect (fixed)

Fix script parsing to produce reliable and speedy <parseresult> outputs

Reported by: David Aspinall Owned by: David Aspinall
Priority: critical Milestone:
Component: 4:prover-isabelle Keywords:
Cc:

Description

See Pure/ProofGeneral?/parsing.ML.

This is an absolutely essential improvement required for Isabelle2007 to have good PGIP support.

Change History (3)

comment:1 Changed 17 years ago by David Aspinall

Suggestions here:

  • Use the existing parser for document output Isar/thy_output
  • Must preserve round trip property: when markup is stripped, syntax input should be returned
  • Later on can think about specifying ways for prover to return different output (probably optionally)
  • Can enhance this to even produce PGML

comment:2 Changed 17 years ago by David Aspinall

Milestone: PG-Eclipse-1.1.0 → PG-Eclipse-1.0.6
Resolution: → fixed
Status: new → closed

Better module now in Isabelle by Makarius. But see #142.

comment:3 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.0.6

Milestone PG-Eclipse-1.0.6 deleted

Note: See TracTickets for help on using tickets.