X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Ftopology%2Fconvert.awk;h=5f72889f78e76ea89f3ee3d6d497192b773b6284;hb=b367de0252e88d6b0476648d5ceac7e4aeffca27;hp=68bcf8a6260599bc629c02f7081213fbe93635ec;hpb=4286d368b6d902a4b54c4cf8590c387f2cdb90ea;p=helm.git

diff --git a/helm/software/matita/nlibrary/topology/convert.awk b/helm/software/matita/nlibrary/topology/convert.awk
index 68bcf8a62..5f72889f7 100644
--- a/helm/software/matita/nlibrary/topology/convert.awk
+++ b/helm/software/matita/nlibrary/topology/convert.awk
@@ -1,7 +1,58 @@
+function process(s) {
+	if(match(s,/^__docfor:(.*)/,data)){
+		s=docfor[data[1]];
+	} 	
+	return s;
+}
+
+function emit(s) {
+	lines[length(lines)] = s;	
+}
+
+function emit_line() {
+	if (! line_done) emit(indent $0);
+	line_done = 0;
+}
+
+function emit_docfor(k) {
+	emit();
+	emit("__docfor:" k);	
+	emit();
+}
+
+function emit_img(key) {
+	emit();
+	emit("![" key "][" key "]");
+	emit();
+}
+
+function done() { line_done = 1; }
+
+function check_begin_docfor(s){
+	if (match(s,/^\(\*D\[([^\]]*)\]/,data)) {
+		curdocblock = data[1];	
+	} else if (match(s,/^D\[([^\]]*)\]/,data)) {
+		curdocblock = data[1];	
+       	} else {
+		curdocblock = "";
+	}
+}
+
+function store_docfor_if_docforblock(s) {
+	if (!line_done && curdocblock != "") {
+		docfor[curdocblock] = docfor[curdocblock] "\n" s;
+		done();
+	}
+}
+
 BEGIN { 
 	do_print = 1; 
 	indent = ""; 
 	refs["matita"] = "http://matita.cs.unibo.it";
+	docfor[0]=""
+	curdocblock="";
+	lines[0]="";
+	line_done =0;
 	} 
 
 # markdown mangling
@@ -9,22 +60,47 @@ BEGIN {
 	match($0, "screenshot *\"([^\"]+)\"", data);
 	key = data[1];
 	refs[key] = key ".png"; 
+	$0 = gensub(/\(\*\* *screenshot[^*]*\*\)/,"",$0);
+	emit_line();
+	emit_img(key);
+	emit_docfor(key);
+	done();
 	}
 
 # literate programming
-/DOCBEGIN/ { 
-	indent = ""; NF = 0; }
-/DOCEND/ { 
-	indent = "    "; NF = 0; } 
+/^\(\*D/ { 
+	check_begin_docfor($0);
+	indent = ""; 
+	done();
+	}
+/^D\[.*\]/ { 
+	check_begin_docfor($0);
+	indent = ""; 
+	done();
+	}
+/^D\*\)/ { 
+	indent = "    "; 
+	curdocblock = "";
+	emit();
+	done();
+	} 
 /HIDE/ { 
 	do_print = 0; }
 { 
-	if (do_print == 1) print indent $0; } 
+	if (do_print == 1) {
+		store_docfor_if_docforblock($0);
+		emit_line(); 
+	}
+	}	
 /UNHIDE/ { 
 	do_print = 1; }
 
 # closing
 END { 
+	print length(lines) > "/dev/stderr";
+	for (i =0; i< length(lines); i++){
+		print process(lines[i]);	
+	}
 	for (i in refs) {
 		print "[" i "]: " refs[i];	
 	}