(* Copyright (C) 2000, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science * Department, University of Bologna, Italy. * * HELM is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or (at your option) any later version. * * HELM is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with HELM; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, * http://cs.unibo.it/helm/. *) module R = Helm_registry module X = HExtlib module T = Types module G = Grafite type script = { name: string; contents: T.items } type status = { helm_dir: string; heading_path: string; heading_lines: int; input_package: string; output_package: string; input_base_uri: string; output_base_uri: string; input_path: string; output_path: string; script_ext: string; coercions: (string * string) list; files: string list; requires: (string * string) list; scripts: script array } let default_script = { name = ""; contents = [] } let default_scripts = 2 let load_registry registry = let suffix = ".conf.xml" in let registry = if Filename.check_suffix registry suffix then registry else registry ^ suffix in Printf.eprintf "reading configuration %s ...\n" registry; flush stderr; R.load_from registry let set_files st = let eof ich = try Some (input_line ich) with End_of_file -> None in let trim l = Filename.chop_extension (Str.string_after l 2) in let cmd = Printf.sprintf "cd %s && find -name *%s" st.input_path st.script_ext in let ich = Unix.open_process_in cmd in let rec aux files = match eof ich with | None -> List.rev files | Some l -> aux (trim l :: files) in let files = aux [] in let _ = Unix.close_process_in ich in {st with files = files} let set_requires st = let map file = (Filename.basename file, file) in let requires = List.rev_map map st.files in {st with requires = requires} let init () = let default_registry = "transcript" in load_registry default_registry let make registry = let id x = x in let get_coercions = R.get_list (R.pair id id) in load_registry registry; let st = { helm_dir = R.get_string "transcript.helm_dir"; heading_path = R.get_string "transcript.heading_path"; heading_lines = R.get_int "transcript.heading_lines"; input_package = R.get_string "package.input_name"; output_package = R.get_string "package.output_name"; input_base_uri = R.get_string "package.input_base_uri"; output_base_uri = R.get_string "package.output_base_uri"; input_path = R.get_string "package.input_path"; output_path = R.get_string "package.output_path"; script_ext = R.get_string "package.script_type"; coercions = get_coercions "package.coercion"; files = []; requires = []; scripts = Array.make default_scripts default_script } in prerr_endline "reading file names ..."; let st = set_files st in let st = set_requires st in st let get_index st name = let rec get_index name i = if i >= Array.length st.scripts then None else if st.scripts.(i).name = name then Some i else get_index name (succ i) in match get_index name 0, get_index "" 0 with | Some i, _ | _, Some i -> i | None, None -> failwith "not enought script entries" let set_items st name items = let i = get_index st name in let script = st.scripts.(i) in let contents = List.rev_append items script.contents in st.scripts.(i) <- {name = name; contents = contents} let set_heading st name = let heading = Filename.concat st.helm_dir st.heading_path, st.heading_lines in set_items st name [T.Heading heading] let set_baseuri st name = let baseuri = Filename.concat st.output_base_uri name in set_items st name [T.BaseUri baseuri] let require st name inc = set_items st name [T.Include inc] let get_coercion st str = try List.assoc str st.coercions with Not_found -> "" let make_path path = List.fold_left Filename.concat "" (List.rev path) let make_prefix path = String.concat "__" (List.rev path) ^ "__" let commit st name = let i = get_index st name in let script = st.scripts.(i) in let path = Filename.concat st.output_path (Filename.dirname name) in let name = Filename.concat st.output_path (name ^ ".ma") in let cmd = Printf.sprintf "mkdir -p %s" path in let _ = Sys.command cmd in let och = open_out name in G.commit och script.contents; close_out och; st.scripts.(i) <- default_script let produce st = let init name = set_heading st name; set_baseuri st name in let partition = function | T.Coercion (false, _) | T.Notation (false, _) -> false | _ -> true in let produce st name = let in_base_uri = Filename.concat st.input_base_uri name in let out_base_uri = Filename.concat st.output_base_uri name in let filter path = function | T.Inline (b, k, obj, p) -> let obj, p = if b then Filename.concat (make_path path) obj, make_prefix path else obj, p in let s = obj ^ G.string_of_inline_kind k in path, Some (T.Inline (b, k, Filename.concat in_base_uri s, p)) | T.Include s -> begin try path, Some (T.Include (List.assoc s st.requires)) with Not_found -> path, None end | T.Coercion (b, obj) -> let str = get_coercion st obj in if str <> "" then path, Some (T.Coercion (b, str)) else let base_uri = if b then out_base_uri else in_base_uri in let s = obj ^ G.string_of_inline_kind T.Con in path, Some (T.Coercion (b, Filename.concat base_uri s)) | T.Section (b, id, _) as item -> let path = if b then id :: path else List.tl path in path, Some item | item -> path, Some item in Printf.eprintf "processing file name: %s ...\n" name; flush stderr; let file = Filename.concat st.input_path (name ^ st.script_ext) in let ich = open_in file in let lexbuf = Lexing.from_channel ich in try let items = V8Parser.items V8Lexer.token lexbuf in close_in ich; let _, rev_items = X.list_rev_map_filter_fold filter [] items in let items = List.rev rev_items in let local_items, global_items = List.partition partition items in let comment = T.Line (Printf.sprintf "From %s" name) in if global_items <> [] then set_items st st.input_package (comment :: global_items); init name; require st name st.input_package; set_items st name local_items; commit st name with e -> prerr_endline (Printexc.to_string e); close_in ich in init st.input_package; require st st.input_package "preamble"; List.iter (produce st) st.files; commit st st.input_package