(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

module F = Filename
module K = Sys

module R = Helm_registry

let template = "../../../matita/matita.ma.templ"

let myself = F.basename Sys.argv.(0)

let rt_base_dir = F.dirname Sys.argv.(0)

let get_preamble () =
  F.concat rt_base_dir template

let copy_preamble preamble och =
  let ich = open_in preamble in
  let rec read () =
    Printf.fprintf och "%s\n" (input_line ich); read ()
  in
  try read () with End_of_file -> close_in ich

let print_header def och =
  let msg = if def then "LOGIC" else "GROUND NOTATION" in
  let stars = String.make (72 - String.length msg) '*' in
  Printf.fprintf och "(* %s %s*)\n\n" msg stars

let print_comment och =
  let msg = Printf.sprintf "NOTE: This file was generated by %s, do not edit" myself in
  let stars = String.make (72 - String.length msg) '*' in
  Printf.fprintf och "(* %s %s*)\n\n" msg stars

let exists_out name =
  let path = [
    R.get_string "xoa.output_dir";
    name
  ] in
  let name = List.fold_left F.concat "" path in
  K.file_exists (name ^ ".ma")

let open_out def preamble name =
  let path = [
    R.get_string "xoa.output_dir";
    name
  ] in
  let name = List.fold_left F.concat "" path in
  let och = open_out (name ^ ".ma") in
  copy_preamble preamble och;
  print_header def och;
  print_comment och;
  och

let out_include och s =
  Printf.fprintf och "include \"%s\".\n\n" s