Admin/website/README
changeset 16572 81778a796290
parent 16312 d13addf9101e
child 16952 9ce755a0d613
equal deleted inserted replaced
16571:c1f41c98fd3c 16572:81778a796290
     1 The Isabelle webpage
     1 The Isabelle Webpage
     2 ====================
     2 ====================
     3 
     3 
     4 (1) philosophy
     4 (1) philosophy
     5 ==============
     5 ==============
     6 
     6 
    51 ==========================
    51 ==========================
    52 
    52 
    53 You may add arbitrary files to the dir structure, but adhere to the following:
    53 You may add arbitrary files to the dir structure, but adhere to the following:
    54 * use XHTML, not loose HTML
    54 * use XHTML, not loose HTML
    55 * only structural markup; if you need layout effects, use CSS
    55 * only structural markup; if you need layout effects, use CSS
       
    56   (browse the exitings files to get some inspirations)
    56 * any files ending with .html are considered as HTML files and are implicitly
    57 * any files ending with .html are considered as HTML files and are implicitly
    57   processed by the preprocessing layer
    58   processed by the preprocessing layer
    58 * for HTML includes, it is most convenient to name them *.include.html to
    59 * for HTML includes, it is most convenient to name them *.include.html to
    59   avoid them to be processed stand-alone by the preprocessing layer
    60   avoid them to be processed stand-alone by the preprocessing layer
    60 * whole dirs maybe selected for statically copying them to the target destination
    61 * whole dirs maybe selected for statically copying them to the
    61   by configuring the project layer
    62   target destination by configuring the project layer
    62 * for attributes etc. referencing file locations, there is a convenient
    63 * for attributes etc. referencing file locations, there is a convenient
    63   abbreviation: "//" at the beginning of a path is translated to the root,
    64   abbreviation: "//" at the beginning of a path is translated to the root,
    64   but expressed relatively to the current location, e. g.
    65   but expressed relatively to the current location, e. g.
    65 
    66 
    66   in abc/def/itsme.html: <a href="//abc/ghi/itsyou.html">
    67   in abc/def/itsme.html: <a href="//abc/ghi/itsyou.html">
    67                 becomes: <a href="../def/itsyou.html">
    68                 becomes: <a href="../def/itsyou.html">
    68 
    69 
    69   Further, targets are checked for existances.
    70   Further, targets are checked for existances.
    70   This is a simple but powerful thing easing to keep the pages consistent.
    71   This is a simple yet powerful thing easing to keep the pages consistent.
    71 * for the semantics of the processing instructions, see build/pypager.py
    72 * for the semantics of the processing instructions, see build/pypager.py
    72   source code
    73   source code
       
    74 
    73 
    75 
    74 (3) using the project layer framework
    76 (3) using the project layer framework
    75 =====================================
    77 =====================================
    76 
    78 
    77 To configure it the first time after checkout, just type
    79 To configure it the first time after checkout, just type