diff options
Diffstat (limited to 'generic/pg-xml.el')
| -rw-r--r-- | generic/pg-xml.el | 33 |
1 files changed, 23 insertions, 10 deletions
diff --git a/generic/pg-xml.el b/generic/pg-xml.el index 79d15b55..18285572 100644 --- a/generic/pg-xml.el +++ b/generic/pg-xml.el @@ -1,14 +1,25 @@ -;; pg-xml.el --- XML functions for Proof General -;; -;; Copyright (C) 2000-2002 LFCS Edinburgh. +;;; pg-xml.el --- XML functions for Proof General + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <David.Aspinall@ed.ac.uk> + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; -;; $Id$ + +;;; Commentary: ;; ;; XML functions for Proof General. ;; +;;; Code: + (require 'cl) (require 'xml) @@ -50,6 +61,7 @@ (defun pg-xml-parse-buffer (&optional buffer nomsg start end) "Parse an XML documment in BUFFER (defaulting to current buffer). +Display progress message unless NOMSG is non-nil. Parsing according to `xml-parse-file' of xml.el. Optional START and END bound the parse." (unless nomsg @@ -72,7 +84,7 @@ Optional START and END bound the parse." (or val (if optional defaultval - (pg-xml-error "pg-xml-get-attr: Didn't find required %s attribute in %s element" + (pg-xml-error "Function pg-xml-get-attr: Didn't find required %s attribute in %s element" attribute (xml-node-name node)))))) (defun pg-xml-child-elts (node) @@ -89,7 +101,7 @@ Optional START and END bound the parse." (xml-node-name node))))) (defun pg-xml-get-child (child node) - "Return single element CHILD of node, give error if more than one." + "Return single element CHILD of NODE, give error if more than one." (let ((children (xml-get-children node child))) (if (> (length children) 1) (progn @@ -130,8 +142,9 @@ Optional START and END bound the parse." ;; based on xml-debug-print from xml.el (defun pg-xml-output-internal (xml indent-string outputfn) - "Outputs the XML tree using OUTPUTFN, which should accept a list of args. -Output with indentation INDENT-STRING (or none if nil)." + "Output the XML tree. +Use indentation INDENT-STRING (or none if nil). +Cal OUTPUTFN, which should accept a list of args." (let ((tree xml) attlist) (funcall outputfn (or indent-string "") "<" (symbol-name (xml-node-name tree))) @@ -156,7 +169,7 @@ Output with indentation INDENT-STRING (or none if nil)." (pg-xml-output-internal node (if indent-string (concat indent-string " ")) outputfn)) ((stringp node) (funcall outputfn node)) (t - (error "pg-xml-output-internal: Invalid XML tree")))) + (error "Function pg-xml-output-internal: Invalid XML tree")))) (funcall outputfn (if indent-string (concat "\n" indent-string) "") "</" (symbol-name (xml-node-name xml)) ">")) |