Re: [isabelle] Unwanted dependency documents in AFP



The HTML will always show all theories that were processed in the current session (it is not affected by the âdocumentâ option). Iâm not aware of a mechanism to suppress them. I.e. this is supposed to happen.

The only thing you could do is a parent session that contains the ones you donât want to see - they will still show up in the HTML of that parent session, though, but at least thereâd be some visual separation.

E.g.:

chapter AFP

session Parity_Game_Base (AFP) = HOL +
 options [timeout = 600]
 theories [document = false]
   "../Coinductive/Coinductive_List"
   "../Graph_Theory/Digraph_Isomorphism"

session Parity_Game (AFP) = Parity_Game_Base +
 options [timeout = 600]
 theories
   PositionalDeterminacy
   AttractorInductive
   Graph_TheoryCompatibility
 document_files
   "root.tex"
   âroot.bib"

Cheers,
Gerwin

> On 16.02.2017, at 03:33, Christoph Dittmann <f-isabellelist at yozora.eu> wrote:
> 
> Hi,
> 
> I noticed that all dependencies show up on this page:
> 
> https://devel.isa-afp.org/browser_info/current/AFP/Parity_Game/index.html
> 
> This is not supposed to happen, but I don't see what I did wrong.
> 
> The ROOT file of Parity_Game is completely analogous to every other ROOT
> file in the AFP, as far as I can tell:
> 
> 
> chapter AFP
> 
> session Parity_Game (AFP) = HOL +
>  options [timeout = 600]
>  theories [document = false]
>    "../Coinductive/Coinductive_List"
>    "../Graph_Theory/Digraph_Isomorphism"
>  theories
>    PositionalDeterminacy
>    AttractorInductive
>    Graph_TheoryCompatibility
>  document_files
>    "root.tex"
>    "root.bib"
> 
> 
> Why do the dependencies show up?
> What can I do to fix this?
> 
> Thanks,
> Christoph
> 



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.