maj script d'extraction de OCaml
Cette révision appartient à :
@@ -1,27 +1,44 @@
|
|||||||
import os
|
import os
|
||||||
|
|
||||||
def extraire_caml(nf_tex, nf_ml, nf_texo, tag) :
|
def extraire_caml(nf_tex, nf_ml, nf_texo, tag) :
|
||||||
|
nf_tex = nf_tex.replace("file://", "")
|
||||||
|
nf_ml = nf_ml.replace("file://", "")
|
||||||
|
nf_texo = nf_texo.replace("file://", "")
|
||||||
output_tex = open(nf_texo, "w")
|
output_tex = open(nf_texo, "w")
|
||||||
output_ml = open(nf_ml, "w")
|
output_ml = open(nf_ml, "w")
|
||||||
incode = False
|
incode = False
|
||||||
nomfonc = ""
|
nomfonc = ""
|
||||||
|
complement = None
|
||||||
|
numfoncAnon = 0
|
||||||
mlref = os.path.basename(nf_ml)
|
mlref = os.path.basename(nf_ml)
|
||||||
for l in open(nf_tex) :
|
for l in open(nf_tex) :
|
||||||
lstrip = l.strip()
|
lstrip = l.strip()
|
||||||
if lstrip == r"\begin{"+tag+"}" :
|
if lstrip.startswith(r"\begin{"+tag+"}") :
|
||||||
incode = True
|
incode = True
|
||||||
nomfonc = ""
|
nomfonc = ""
|
||||||
|
complement = None
|
||||||
|
if "[" in lstrip :
|
||||||
|
complement = lstrip.split("[")[1].split("]")[0]
|
||||||
continue
|
continue
|
||||||
if incode :
|
if incode :
|
||||||
if nomfonc == "" and "let" in lstrip :
|
if nomfonc == "" :
|
||||||
nomfonc = l[4:]
|
if lstrip == "" :
|
||||||
if nomfonc.startswith("rec ") :
|
continue
|
||||||
nomfonc = nomfonc[4:]
|
if "let" in lstrip :
|
||||||
nomfonc = nomfonc.split()[0]
|
nomfonc = l[4:]
|
||||||
|
if nomfonc.startswith("rec ") :
|
||||||
|
nomfonc = nomfonc[4:]
|
||||||
|
nomfonc = nomfonc.split()[0]
|
||||||
|
else :
|
||||||
|
nomfonc = "anon" + str(numfoncAnon)
|
||||||
|
numfoncAnon += 1
|
||||||
output_ml.write("(*** " + nomfonc + " ***)\n")
|
output_ml.write("(*** " + nomfonc + " ***)\n")
|
||||||
if lstrip == r"\end{"+tag+"}" :
|
if lstrip == r"\end{"+tag+"}" :
|
||||||
output_ml.write("(*** " + nomfonc + "_fin ***)\n\n")
|
output_ml.write("(*** " + nomfonc + "_fin ***)\n\n")
|
||||||
output_tex.write(r"\lstinputcaml[linerange="+nomfonc+"-"+nomfonc+"_fin]{"+ mlref + "}\n")
|
if complement is not None :
|
||||||
|
output_tex.write(r"\inputcaml["+nomfonc+"]{"+ mlref + "}["+complement+"]\n")
|
||||||
|
else :
|
||||||
|
output_tex.write(r"\inputcaml["+nomfonc+"]{"+ mlref + "}\n")
|
||||||
incode = False
|
incode = False
|
||||||
continue
|
continue
|
||||||
output_ml.write(l)
|
output_ml.write(l)
|
||||||
|
|||||||
Référencer dans un nouveau ticket
Bloquer un utilisateur