diff options
Diffstat (limited to 'ide/ideutils.ml')
| -rw-r--r-- | ide/ideutils.ml | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 0977a18906..1786957597 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) @@ -69,6 +71,12 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let set_location = ref (function s -> failwith "not ready") +let display_location ins = + let line = ins#line + 1 in + let off = ins#line_offset + 1 in + let msg = Printf.sprintf "Line: %5d Char: %3d" line off in + !set_location msg + (** A utf8 char is either a single byte (ascii char, 0xxxxxxx) or multi-byte (with a leading byte 11xxxxxx and extra bytes 10xxxxxx) *) @@ -465,4 +473,3 @@ let browse_keyword prerr text = let u = Lazy.force url_for_keyword text in browse prerr (doc_url() ^ u) with Not_found -> prerr ("No documentation found for \""^text^"\".\n") - |