ProverKnowledge updates and improvements

[David Aspinall <da+pgtrac@…>]

Various desirable improvements:

• Fix output conversion from XML PGIP into HTML (partly complete)
• Port to using PGIP commands (may need PGIP extensions, although askids/setids already used in Proof Objects view)
• Support cached knowledge in different contexts and top-level lookups
  (may need Isabelle support)
• Connect to Proof Objects view (partly complete)

Other possible, more tentative improvements:

• Add search and filtering facilities, e.g. based on matching theorem content/names
• Add dependency knowledge based on <metainforesponse>
• Consider persisting some of knowledge (for names at least)

What we need really in PGIP is some clear notion of context/namespace which can be treated generically in the interface.

[David Aspinall <da+pgtrac@…>]

There are a few small glitches to fix:

• Display "unknown" (or empty string) instead of "null" for unknown type
• Deal with output that has several theorems (may be OK with <showid>)
• Allow cancellation of callback in loadFullyBg
• Consistency with proof state during script management needs review after changes to script management

The performance is actually pretty slick now: even loading 8000-odd identifiers for the Proof Objects view is swift. So some of the suggestions above for caching and persisting don't really seem that necessary/urgent.

[David Aspinall <da+pgtrac@…>]

More hints on PGIP needed in ProverKnowledge:

   <showid thyname="X" objtype="Y" name="Z"/>  

Asks to know the value of a given identifier. The response will be of the form:

   <idvalue thyname="X" objtype="Y" name="Z"><pgmltext>....</pgmltext></idvalue>

The thyname attribute is optional and shouldn't be given for a fully qualified name in Isabelle. The three attributes and names are the same as those used in <askids> and <setids>.

The code should cache idvalue responses automatically in the knowledge by a listener for <idvalue>: the prover is free to send these when it feels like, not necessarily as a result of <idvalue>. (E.g. a smart prover or the broker may update values previously inspected when they change).

When the UI wants to update a particular display of an item and issue a <showid>, it should use a callback, blocking call or one-time listener from the command queue.

(NB: we should gradually refactor the outdating support in Prover Knowledge to move it to the internal broker).

[David Aspinall]

Other snippets of ML code currently called by ProverKnowledge are:

• To find the path for searching for theory files in the loaded library:

  map (Path.implode o Path.expand o Path.explode) (show_path ())
  

• To find the methods available in a given theory

  print_methods (theory "NewTheory");
  

• To find the ancestors of a given theory:

  Theory.ancestors_of (theory "NewTheory");
  

(previously used Theory.sign_of: should check whether new call has right output format)

• To find axioms:

  commas (map (fst) (axioms_of (theory "Set")));
  

• To find theorems:

  commas (map (fst) (PureThy.thms_of (theory "ATP_Linkup")));
  

[David Aspinall]

Milestone PG-Eclipse-1.0.6 deleted