]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/nlibrary/topology/convert.awk
Preparing for 0.5.9 release.
[helm.git] / helm / software / matita / nlibrary / topology / convert.awk
1 function process(s) {
2         if(match(s,/^__docfor:(.*)/,data)){
3                 s=docfor[data[1]];
4         }       
5         return s;
6 }
7
8 function emit(s) {
9         lines[length(lines)] = s;       
10 }
11
12 function emit_line() {
13         if (! line_done) emit(indent $0);
14         line_done = 0;
15 }
16
17 function emit_docfor(k) {
18         emit();
19         emit("__docfor:" k);    
20         emit();
21 }
22
23 function emit_img(key) {
24         emit();
25         emit("![" key "][" key "]");
26         emit();
27 }
28
29 function done() { line_done = 1; }
30
31 function check_begin_docfor(s){
32         if (match(s,/^\(\*D\[([^\]]*)\]/,data)) {
33                 curdocblock = data[1];  
34         } else if (match(s,/^D\[([^\]]*)\]/,data)) {
35                 curdocblock = data[1];  
36         } else {
37                 curdocblock = "";
38         }
39 }
40
41 function store_docfor_if_docforblock(s) {
42         if (!line_done && curdocblock != "") {
43                 docfor[curdocblock] = docfor[curdocblock] "\n" s;
44                 done();
45         }
46 }
47
48 BEGIN { 
49         do_print = 1; 
50         indent = ""; 
51         refs["matita"] = "http://matita.cs.unibo.it";
52         docfor[0]=""
53         curdocblock="";
54         lines[0]="";
55         line_done =0;
56         } 
57
58 # markdown mangling
59 /screenshot *".*"/ { 
60         match($0, "screenshot *\"([^\"]+)\"", data);
61         key = data[1];
62         refs[key] = key ".png"; 
63         $0 = gensub(/\(\*\* *screenshot[^*]*\*\)/,"",$0);
64         emit_line();
65         emit_img(key);
66         emit_docfor(key);
67         done();
68         }
69
70 # literate programming
71 /^\(\*D/ { 
72         check_begin_docfor($0);
73         indent = ""; 
74         done();
75         }
76 /^D\[.*\]/ { 
77         check_begin_docfor($0);
78         indent = ""; 
79         done();
80         }
81 /^D\*\)/ { 
82         indent = "    "; 
83         curdocblock = "";
84         emit();
85         done();
86         } 
87 /HIDE/ { 
88         do_print = 0; }
89
90         if (do_print == 1) {
91                 store_docfor_if_docforblock($0);
92                 emit_line(); 
93         }
94         }       
95 /UNHIDE/ { 
96         do_print = 1; }
97
98 # closing
99 END { 
100         print length(lines) > "/dev/stderr";
101         for (i =0; i< length(lines); i++){
102                 print process(lines[i]);        
103         }
104         for (i in refs) {
105                 print "[" i "]: " refs[i];      
106         }
107