Changes between Initial Version and Version 1 of Ticket #79


Ignore:
Timestamp:
Feb 25, 2007, 1:36:21 PM (17 years ago)
Author:
David Aspinall
Comment:

The starting points for this have been added: see the symbol table DTD in config/symbols, and includeSymbolFile in !HTMLSymbols.java

Legend:

Unmodified
Added
Removed
Modified

  • Ticket #79 – Description

    initial v1  
    88We need to support several tables.  Perhaps the easiest way is to add a directive:
    99
    10  * <includetable file="XXX">
     10 * <includesymbolfile name="config/Isabelle.sym">
    1111
    1212to the symbol table DTD.  File may be absolute or installation-relative.  The symbol table editor needs to support table inclusion, also comment elements.  It should be possible to load the default tables, create an empty table, as well as select the project-specific table.  This should be set as a project-specific property.  The present workspace-specific preference may be used as the default; however we would like to select the default by examining the platform (which requires