src/Pure/Thy/browser_info.ML
changeset 3639 dc998476ce76
parent 3628 41a49c671901
child 3748 e5d2399a154f
equal deleted inserted replaced
3638:2b67561c6488 3639:dc998476ce76
    92         val rpath = if p subdir_of (!base_path) then relative_path (!base_path) p
    92         val rpath = if p subdir_of (!base_path) then relative_path (!base_path) p
    93                     else relative_path (normalize_path (!home_path)) p;
    93                     else relative_path (normalize_path (!home_path)) p;
    94     in tack_on base rpath end
    94     in tack_on base rpath end
    95 in
    95 in
    96   val html_path = make_path "html";
    96   val html_path = make_path "html";
    97   val graph_path = make_path "graph"
    97   val graph_path = make_path "graph/data"
    98 end;
    98 end;
    99 
    99 
   100 
   100 
   101 (*Location of theory-list.txt and index.html (set by init_html)*)
   101 (*Location of theory-list.txt and index.html (set by init_html)*)
   102 val index_path = ref "";
   102 val index_path = ref "";