← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to interp/dumpglob.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
interp/dumpglob.ml
1
1
(************************************************************************)
2
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
3
 
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 
3
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
4
4
(*   \VV/  **************************************************************)
5
5
(*    //   *      This file is distributed under the terms of the       *)
6
6
(*         *       GNU Lesser General Public License Version 2.1        *)
7
7
(************************************************************************)
8
8
 
9
 
(* $Id: dumpglob.ml 13674 2010-12-04 10:34:11Z herbelin $ *)
 
9
(* $Id: dumpglob.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
10
10
 
11
11
 
12
12
(* Dump of globalization (to be used by coqdoc) *)
110
110
    (* Theorem/Lemma outside its outer section of definition *)
111
111
    dir
112
112
 
 
113
let interval loc =
 
114
  let loc1,loc2 = Util.unloc loc in
 
115
  loc1, loc2-1
 
116
 
113
117
let dump_ref loc filepath modpath ident ty =
114
 
  dump_string (Printf.sprintf "R%d %s %s %s %s\n"
115
 
                  (fst (Util.unloc loc)) filepath modpath ident ty)
 
118
  let bl,el = interval loc in
 
119
  dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
 
120
                  bl el filepath modpath ident ty)
116
121
 
117
122
let add_glob_gen loc sp lib_dp ty =
118
123
  if dump () then
144
149
let dump_binding loc id = ()
145
150
 
146
151
let dump_definition (loc, id) sec s =
147
 
  dump_string (Printf.sprintf "%s %d %s %s\n" s (fst (Util.unloc loc))
 
152
  let bl,el = interval loc in
 
153
  dump_string (Printf.sprintf "%s %d:%d %s %s\n" s bl el
148
154
                        (Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
149
155
 
150
156
let dump_reference loc modpath ident ty =
151
 
  dump_string (Printf.sprintf "R%d %s %s %s %s\n"
152
 
                  (fst (Util.unloc loc)) (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
 
157
  let bl,el = interval loc in
 
158
  dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
 
159
                  bl el (Names.string_of_dirpath (Lib.library_dp ())) modpath ident ty)
153
160
 
154
161
let dump_constraint ((loc, n), _, _) sec ty =
155
162
  match n with
167
174
    let l = if l = [] then l else Util.list_drop_last l in
168
175
    let fp = Names.string_of_dirpath dp in
169
176
    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
170
 
      dump_string (Printf.sprintf "R%d %s %s %s %s\n"
171
 
                      (fst (Util.unloc loc)) fp mp "<>" ty)
 
177
    let bl,el = interval loc in
 
178
      dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
 
179
                      bl el fp mp "<>" ty)
172
180
 
173
181
let dump_moddef loc mp ty =
174
182
  if dump () then
 
183
    let bl,el = interval loc in
175
184
    let (dp, l) = Lib.split_modpath mp in
176
185
    let mp = Names.string_of_dirpath (Names.make_dirpath l) in
177
 
      dump_string (Printf.sprintf "%s %d %s %s\n" ty (fst (Util.unloc loc)) "<>" mp)
 
186
      dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el "<>" mp)
178
187
 
179
188
let dump_libref loc dp ty =
180
 
  dump_string (Printf.sprintf "R%d %s <> <> %s\n"
181
 
                  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
 
189
  let bl,el = interval loc in
 
190
  dump_string (Printf.sprintf "R%d:%d %s <> <> %s\n"
 
191
                  bl el (Names.string_of_dirpath dp) ty)
182
192
 
183
193
let cook_notation df sc =
184
194
  (* We encode notations so that they are space-free and still human-readable *)