diff options
author | Quentin Carbonneaux <quentin.carbonneaux@yale.edu> | 2016-03-08 22:12:38 -0500 |
---|---|---|
committer | Quentin Carbonneaux <quentin.carbonneaux@yale.edu> | 2016-03-08 22:15:54 -0500 |
commit | 03f853b6e791d8005586c219493bda7324044b9e (patch) | |
tree | d01db50e26ce548f4e65d6d0a1370a191aaa4500 /doc | |
parent | fc1a998292338d0144961591ebcd9373c2b80faf (diff) | |
download | roux-03f853b6e791d8005586c219493bda7324044b9e.tar.gz |
pheeew, fix numbered titles
Diffstat (limited to 'doc')
-rw-r--r-- | doc/txt.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/doc/txt.ml b/doc/txt.ml index 7414b11..a753cc3 100644 --- a/doc/txt.ml +++ b/doc/txt.ml @@ -10,6 +10,8 @@ and item = let (|>) x f = f x +let isspace = String.contains " \n\t" + module String = struct include String @@ -22,6 +24,15 @@ module String = struct let lp = String.length p in String.length s >= lp && p = String.sub s 0 lp + + let trim s = + let l = String.length s in + let i = ref 0 and j = ref (l-1) in + while !i<l && isspace s.[!i] + do incr i done; + while !j>=0 && isspace s.[!j] + do decr j done; + if !j = -1 then s else sub s !i (!j- !i+1) end let warn = Printf.eprintf @@ -66,7 +77,7 @@ let skipbul s = String.suff s (endbul s) let gettitles lines = let titles = Hashtbl.create 100 in let insert lvl n t = - let t = skipnum (String.suff t 2) in + let t = String.trim (skipnum (String.suff t 2)) in if Hashtbl.mem titles t then warn "line %d: title has multiple definitions\n" n; Hashtbl.add titles t (lvl, n) in @@ -199,7 +210,6 @@ type printer = let print pp s = let l = String.length s in - let isspace = String.contains " \n\t" in let rec getlink j spc = if j >= l || s.[j] = '>' then j+1, "" else if isspace s.[j] then @@ -212,9 +222,7 @@ let print pp s = j', Printf.sprintf "%c%s" s.[j] t in let getlink j = let j', s = getlink j false in - if isspace s.[0] - then j', String.suff s 1 - else j', s in + j', String.trim s in let rec getdlim j d = if j >= l || s.[j] = d then j+1, "" else let j', t = getdlim (j+1) d in |