]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/binaries/transcript/engine.ml
transcript: very alpha version.
[helm.git] / helm / software / components / binaries / transcript / engine.ml
1 (* Copyright (C) 2000, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 module R = Helm_registry
27
28 type script = {
29    name: string;
30    contents: Types.items
31 }
32
33 type status = {
34    helm_dir: string;
35    heading_path: string;
36    heading_lines: int;
37    package: string;
38    base_uri: string;
39    input_path: string;
40    output_path: string;
41    script_ext: string;
42    files: string list;
43    requires: (string * string) list;
44    scripts: script array
45 }
46
47 let default_script = { 
48    name = ""; contents = []
49 }
50
51 let default_scripts = 2
52
53 let load_registry registry =
54    let suffix = ".conf.xml" in
55    let registry = 
56       if Filename.check_suffix registry suffix then registry
57       else registry ^ suffix
58    in
59    Printf.eprintf "reading configuration %s ...\n" registry; flush stderr;
60    R.load_from registry
61
62 let set_files st =
63    let eof ich = try Some (input_line ich) with End_of_file -> None in
64    let trim l = Filename.chop_extension (Str.string_after l 2) in
65    let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.script_ext in
66    let ich = Unix.open_process_in cmd in
67    let rec aux files =
68       match eof ich with
69          | None   -> List.rev files
70          | Some l -> aux (trim l :: files)
71    in 
72    let files = aux [] in
73    let _ = Unix.close_process_in ich in
74    {st with files = files}
75
76 let set_requires st =
77    let map file = (Filename.basename file, file) in
78    let requires = List.rev_map map st.files in
79    {st with requires = requires}
80
81 let init () = 
82    let default_registry = "transcript" in
83    load_registry default_registry
84
85 let make registry =
86    load_registry registry;
87    let st = {
88       helm_dir = R.get_string "transcript.helm_dir";
89       heading_path = R.get_string "transcript.heading_path";
90       heading_lines = R.get_int "transcript.heading_lines";
91       package = R.get_string "package.name";
92       base_uri = R.get_string "package.base_uri";
93       input_path = R.get_string "package.input_path";
94       output_path = R.get_string "package.output_path";
95       script_ext = R.get_string "package.script_type";
96       files = [];
97       requires = [];
98       scripts = Array.make default_scripts default_script
99    } in
100    prerr_endline "reading file names ...";
101    let st = set_files st in
102    let st = set_requires st in
103    st
104
105 let get_index st name = 
106    let rec get_index name i =
107       if i >= Array.length st.scripts then None else 
108       if st.scripts.(i).name = name then Some i else 
109       get_index name (succ i)
110    in
111    match get_index name 0, get_index "" 0 with
112       | Some i, _ | _, Some i -> i
113       | None, None            -> failwith "not enought script entries"
114
115 let set_items st name items =
116    let i = get_index st name in
117    let script = st.scripts.(i) in
118    let contents = List.rev_append items script.contents in
119    st.scripts.(i) <- {name = name; contents = contents}
120    
121 let set_heading st name =
122    let heading = Filename.concat st.helm_dir st.heading_path, st.heading_lines in
123    set_items st name [Types.Heading heading] 
124    
125 let set_baseuri st name =
126    let baseuri = Filename.concat st.base_uri name in
127    set_items st name [Types.BaseUri baseuri]
128    
129 let commit st name =
130    let i = get_index st name in
131    let script = st.scripts.(i) in
132    let path = Filename.concat st.output_path (Filename.dirname name) in
133    let name = Filename.concat st.output_path (name ^ ".ma") in
134    let cmd = Printf.sprintf "mkdir -p %s" path in
135    let _ = Sys.command cmd in
136    let och = open_out name in
137    Grafite.commit och script.contents;
138    close_out och;
139    st.scripts.(i) <-  default_script
140    
141 let produce st =
142    let init name = set_heading st name; set_baseuri st name in
143    let produce st name =
144       Printf.eprintf "processing file name: %s ...\n" name; flush stderr; 
145       let file = Filename.concat st.input_path (name ^ st.script_ext) in
146       let ich = open_in file in
147       let lexbuf = Lexing.from_channel ich in
148       try 
149          let items = V8Parser.items V8Lexer.token lexbuf in
150          close_in ich;
151          init name; set_items st name items; commit st name
152       with e -> 
153          prerr_endline (Printexc.to_string e); close_in ich 
154    in
155    init st.package; List.iter (produce st) st.files; commit st st.package