-<?xml version="1.0"?>
-<!DOCTYPE article PUBLIC "-//OASIS//DTD DocBook XML V4.1.2//EN"
- "http://www.oasis-open.org/docbook/xml/4.1.2/docbookx.dtd" [
- <!ENTITY legal SYSTEM "legal.xml">
- <!ENTITY appversion "0.0">
- <!ENTITY manrevision "0.0">
- <!ENTITY date "February 2006">
- <!ENTITY app "<application>Matita</application>">
- <!ENTITY appname "Matita">
- <!ENTITY version "0.0">
+<?xml version='1.0' encoding='UTF-8'?>
+<!DOCTYPE refentry PUBLIC "-//OASIS//DTD DocBook XML V4.2//EN"
+ "http://www.oasis-open.org/docbook/xml/4.2/docbookx.dtd" [
+
+ <!ENTITY dhfirstname "<firstname>Enrico</firstname>">
+ <!ENTITY dhsurname "<surname>Tassi</surname>">
+ <!ENTITY dhdate "<date>21 Jun 2007</date>">
+ <!ENTITY dhsection "<manvolnum>1</manvolnum>">
+ <!ENTITY dhemail "<email>gareuselesinge@debian.org</email>">
+ <!ENTITY dhusername "Enrico Tassi">
+ <!ENTITY dhucpackage "<refentrytitle>matita</refentrytitle>">
+ <!ENTITY dhpackage "matita">
+
+ <!ENTITY debian "<productname>Debian</productname>">
+ <!ENTITY gnu "<acronym>GNU</acronym>">
+ <!ENTITY gpl "&gnu; <acronym>GPL</acronym>">
]>
-<!-- =============Document Header ============================= -->
-<article id="index" lang="en">
-<!-- please do not change the id; for translations, change lang to -->
-<!-- appropriate code -->
-<articleinfo>
- <title>&app; Manual V&manrevision;</title>
+<refentry>
+ <refentryinfo>
+ <address>
+ &dhemail;
+ </address>
+ <author>
+ &dhfirstname;
+ &dhsurname;
+ </author>
+ <copyright>
+ <year>2007</year>
+ <holder>&dhusername;</holder>
+ </copyright>
+ &dhdate;
+ </refentryinfo>
+ <refmeta>
+ &dhucpackage;
+
+ &dhsection;
+ </refmeta>
+ <refnamediv>
+ <refname>&dhpackage;</refname>
+
+ <refpurpose>creates XML data file for Vim7 omni completion from
+ DTDs</refpurpose>
+ </refnamediv>
+ <refsynopsisdiv>
+ <cmdsynopsis>
+ <command>&dhpackage;</command>
+ <arg choice="req"><replaceable>filename</replaceable>.dtd</arg>
+ <arg choice="opt"><replaceable>dialectname</replaceable></arg>
+ </cmdsynopsis>
+ </refsynopsisdiv>
+
+ <refsect1>
+ <title>DESCRIPTION</title>
+
+ <para> This manual page documents brieftly the
+ <command>&dhpackage;</command> program. For more information see its HTML
+ documentation in
+ <filename>/usr/share/doc/vim-scripts/html/dtd2vim.html</filename>.
+ </para>
+
+ <para>Starting from version 7 Vim supports context aware completion of XML
+ files (and others). In particular, when the file being edited is an XML
+ file, completion can be driven by the grammar extracted from a Document
+ Type Definition (DTD). </para>
+
+ <para>For this feature to work the user should put an XML data file
+ corresponding to the desired DTD in a <filename>autoload/xml</filename>
+ directory contained in a directory belonging to Vim's
+ <varname>'runtimepath'</varname> (for example
+ <filename>~/.vim/autoload/xml/</filename>). </para>
+
+ <para><command>&dhpackage;</command> is the program that creates XML data
+ files from DTDs. Given as input a DTD
+ <filename><replaceable>file</replaceable>.dtd</filename> it will create a
+ <filename>file.vim</filename> XML data file.
+ <replaceable>dialectname</replaceable> will be part of dictionary name
+ and will be used as argument for the <command>:XMLns</command> command.
+ </para>
+
+ </refsect1>
+
+ <refsect1>
+ <title>OPTIONS</title>
+
+ <para>None. </para>
+ </refsect1>
+
+ <refsect1>
+ <title>SEE ALSO</title>
+
+ <para>vim (1).</para>
+
+ <para>In the Vim online help: <userinput>:help compl-omni</userinput>,
+ <userinput>:help ft-xml-omni</userinput>, <userinput>:help
+ :XMLns</userinput>. </para>
+
+ <para>dtd2vim is fully documented in
+ <filename>/usr/share/doc/vim-scripts/html/dtd2vim.html</filename>.
+ </para>
+ </refsect1>
+
+ <refsect1>
+ <title>AUTHOR</title>
+
+ <para>This manual page was written by &dhusername; &dhemail; for the
+ &debian; system (but may be used by others). Permission is granted to
+ copy, distribute and/or modify this document under the terms of the &gnu;
+ General Public License, Version 2 any later version published by the Free
+ Software Foundation. </para>
+
+ <para> On Debian systems, the complete text of the GNU General Public
+ License can be found in /usr/share/common-licenses/GPL. </para>
+ </refsect1>
+
+</refentry>
- <copyright>
- <year>2006</year>
- <holder>The HELM team.</holder>
- </copyright>
-<!-- translators: uncomment this:
-
- <copyright>
- <year>2002</year>
- <holder>ME-THE-TRANSLATOR (Latin translation)</holder>
- </copyright>
-
- -->
-<!-- An address can be added to the publisher information. If a role is
- not specified, the publisher/author is the same for all versions of the
- document. -->
-<!-- CSC:
- <publisher>
- <publishername> GNOME Documentation Project </publishername>
- </publisher>
--->
-
- &legal;
- <!-- This file contains link to license for the documentation (GNU FDL), and
- other legal stuff such as "NO WARRANTY" statement. Please do not change
- any of this. -->
-
- <authorgroup>
- <author>
- <firstname>Andrea</firstname>
- <surname>Asperti</surname>
- <affiliation>
- <address> <email>asperti@cs.unibo.it</email> </address>
- </affiliation>
- </author>
- <author>
- <firstname>Claudio</firstname>
- <surname>Sacerdoti Coen</surname>
- <affiliation>
- <address> <email>sacerdot@cs.unibo.it</email> </address>
- </affiliation>
- </author>
- <author>
- <firstname>Enrico</firstname>
- <surname>Tassi</surname>
- <affiliation>
- <address> <email>tassi@cs.unibo.it</email> </address>
- </affiliation>
- </author>
- <author>
- <firstname>Stefano</firstname>
- <surname>Zacchiroli</surname>
- <affiliation>
- <address> <email>zacchiro@cs.unibo.it</email> </address>
- </affiliation>
- </author>
-<!-- This is appropriate place for other contributors: translators,
- maintainers, etc. Commented out by default.
- <othercredit role="translator">
- <firstname>Latin</firstname>
- <surname>Translator 1</surname>
- <affiliation>
- <orgname>Latin Translation Team</orgname>
- <address> <email>translator@gnome.org</email> </address>
- </affiliation>
- <contrib>Latin translation</contrib>
- </othercredit>
--->
- </authorgroup>
-
-<revhistory>
- <revision>
- <revnumber>&appname; Manual V&manrevision;</revnumber>
- <date>&date;</date>
- <revdescription>
- <para role="author">The HELM team
-<!--
- <email>baudais@okstate.edu</email>
--->
- </para>
-<!--
- <para role="publisher">GNOME Documentation Project</para>
--->
- </revdescription>
- </revision>
- <revision>
- <revnumber>0.0</revnumber>
- <date>4 February 2006</date>
- <authorinitials>HELM</authorinitials>
- <revremark>
- First draft completed.
- </revremark>
- </revision>
-
- </revhistory>
-
- <releaseinfo>This manual describes version &appversion; of &appname;.
- </releaseinfo>
- <!-- The following feedback information only applies to appliactions
- listed in bugzilla.gnome.org and bugzilla.ximian.com. For other
- applications, please provide your own feedback info or remove thsi
- section altogether -->
- <legalnotice>
- <title>Feedback</title>
- <para>To report a bug or make a suggestion regarding the &app; application or
- this manual, follow the directions in the
- <ulink url="http://mowgli.cs.unibo.it/bugs"
- type="help">HELM Bugzilla Page</ulink>.
- </para>
-<!-- Translators may also add here feedback address for translations -->
- </legalnotice>
-
-</articleinfo>
-
- <indexterm zone="index">
- <primary>Matita</primary>
- </indexterm>
-
-<!-- ============= Document Body ============================= -->
-<!-- ============= Introduction ============================== -->
-<sect1 id="intro">
- <title>Introduction</title>
- <sect2 id="what">
- <title>What is Matita?</title>
-
- <para>
- <application>Matita</application> is a proof assistant for ...
- </para>
-
- </sect2>
-</sect1>
-
-<!-- =========== Terms, declarations and definitions ============ -->
-<sect1 id="terms_decl_def">
- <title>Terms, definitions, declarations and proofs</title>
- <sect2 id="terms">
- <title>Terms</title>
- </sect2>
- <sect2 id="definitions">
- <title>Definitions</title>
- </sect2>
- <sect2 id="declarations">
- <title>Declarations (of inductive types)</title>
- </sect2>
- <sect2 id="proofs">
- <title>Proofs</title>
- </sect2>
-</sect1>
-
-<!-- ============ Tactics ====================== -->
-<sect1 id="tactics">
- <title>Tactics</title>
-
- <sect2 id="absurd">
- <title>absurd <term></title>
- <para>The tactic <command>absurd</command> </para>
-<para>
-<ulink url="#terms">ciao</ulink>
-</para>
- </sect2>
- <sect2 id="apply">
- <title>apply <term></title>
- <para>The tactic <command>apply</command> </para>
- </sect2>
- <sect2 id="assumption">
- <title>assumption</title>
- <para>The tactic <command>assumption</command> </para>
- </sect2>
- <sect2 id="auto">
- <title>auto [depth=<int>] [width=<int>] [paramodulation] [full]</title>
- <para>The tactic <command>auto</command> </para>
- </sect2>
- <sect2 id="clear">
- <title>clear <id></title>
- <para>The tactic <command>clear</command> </para>
- </sect2>
- <sect2 id="clearbody">
- <title>clearbody <id></title>
- <para>The tactic <command>clearbody</command> </para>
- </sect2>
- <sect2 id="change">
- <title>change <pattern> with <term></title>
- <para>The tactic <command>change</command> </para>
- </sect2>
- <sect2 id="compare">
- <title>compare <term></title>
- <para>The tactic <command>compare</command> </para>
- </sect2>
- <sect2 id="constructor">
- <title>constructor <int></title>
- <para>The tactic <command>constructor</command> </para>
- </sect2>
- <sect2 id="contradiction">
- <title>contradiction</title>
- <para>The tactic <command>contradiction</command> </para>
- </sect2>
- <sect2 id="cut">
- <title>cut <term> [as <id>]</title>
- <para>The tactic <command>cut</command> </para>
- </sect2>
- <sect2 id="decide equality">
- <title>decide</title>
- <para>The tactic <command>decide equality</command> </para>
- </sect2>
- <sect2 id="decompose">
- <title>decompose [<ident list>] <ident> [<intros_spec>]</title>
- <para>The tactic <command>decompose</command> </para>
- </sect2>
- <sect2 id="discriminate">
- <title>discriminate <term></title>
- <para>The tactic <command>discriminate</command> </para>
- </sect2>
- <sect2 id="elim">
- <title>elim <term> [using <term>] [<intros_spec>]</title>
- <para>The tactic <command>elim</command> </para>
- </sect2>
- <sect2 id="elimType">
- <title>elimType <term> [using <term>]</title>
- <para>The tactic <command>elimType</command> </para>
- </sect2>
- <sect2 id="exact">
- <title>exact <term></title>
- <para>The tactic <command>exact</command> </para>
- </sect2>
- <sect2 id="exists">
- <title>exists</title>
- <para>The tactic <command>exists</command> </para>
- </sect2>
- <sect2 id="fail">
- <title>fail</title>
- <para>The tactic <command>fail</command> </para>
- </sect2>
- <sect2 id="fold">
- <title>fold <reduction_kind> <term> <pattern></title>
- <para>The tactic <command>fold</command> </para>
- </sect2>
- <sect2 id="fourier">
- <title>fourier</title>
- <para>The tactic <command>fourier</command> </para>
- </sect2>
- <sect2 id="fwd">
- <title>fwd <ident> [<ident list>]</title>
- <para>The tactic <command>fwd</command> </para>
- </sect2>
- <sect2 id="generalize">
- <title>generalize <pattern> [as <id>]</title>
- <para>The tactic <command>generalize</command> </para>
- </sect2>
- <sect2 id="id">
- <title>id</title>
- <para>The tactic <command>id</command> </para>
- </sect2>
- <sect2 id="injection">
- <title>injection <term></title>
- <para>The tactic <command>injection</command> </para>
- </sect2>
- <sect2 id="intro">
- <title>intro [<ident>]</title>
- <para>The tactic <command>intro</command> </para>
- </sect2>
- <sect2 id="intros">
- <title>intros <intros_spec></title>
- <para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="inversion">
- <title>intros <term></title>
- <para>The tactic <command>intros</command> </para>
- </sect2>
- <sect2 id="lapply">
- <title>lapply [depth=<int>] <term> [to <term list] [using <ident>]</title>
- <para>The tactic <command>lapply</command> </para>
- </sect2>
- <sect2 id="left">
- <title>left</title>
- <para>The tactic <command>left</command> </para>
- </sect2>
- <sect2 id="letin">
- <title>letin <ident> ≝ <term></title>
- <para>The tactic <command>letin</command> </para>
- </sect2>
- <sect2 id="normalize">
- <title>normalize <pattern></title>
- <para>The tactic <command>normalize</command> </para>
- </sect2>
- <sect2 id="paramodulation">
- <title>paramodulation <pattern></title>
- <para>The tactic <command>paramodulation</command> </para>
- </sect2>
- <sect2 id="reduce">
- <title>reduce <pattern></title>
- <para>The tactic <command>reduce</command> </para>
- </sect2>
- <sect2 id="reflexivity">
- <title>reflexivity</title>
- <para>The tactic <command>reflexivity</command> </para>
- </sect2>
- <sect2 id="replace">
- <title>replace <pattern> with <term></title>
- <para>The tactic <command>replace</command> </para>
- </sect2>
- <sect2 id="rewrite">
- <title>rewrite {<|>} <term> <pattern></title>
- <para>The tactic <command>rewrite</command> </para>
- </sect2>
- <sect2 id="right">
- <title>right</title>
- <para>The tactic <command>right</command> </para>
- </sect2>
- <sect2 id="ring">
- <title>ring</title>
- <para>The tactic <command>ring</command> </para>
- </sect2>
- <sect2 id="simplify">
- <title>simplify <pattern></title>
- <para>The tactic <command>simplify</command> </para>
- </sect2>
- <sect2 id="split">
- <title>split</title>
- <para>The tactic <command>split</command> </para>
- </sect2>
- <sect2 id="symmetry">
- <title>symmetry</title>
- <para>The tactic <command>symmetry</command> </para>
- </sect2>
- <sect2 id="transitivity">
- <title>transitivity <term></title>
- <para>The tactic <command>transitivity</command> </para>
- </sect2>
- <sect2 id="unfold">
- <title>unfold [<term>] <pattern></title>
- <para>The tactic <command>unfold</command> </para>
- </sect2>
- <sect2 id="whd">
- <title>whd <pattern></title>
- <para>The tactic <command>whd</command> </para>
- </sect2>
-
-</sect1>
-
- <!-- ============= Application License ============================= -->
-
- <sect1 id="license">
- <title>License</title>
- <para>
- This program is free software; you can redistribute it and/or
- modify it under the terms of the <citetitle>GNU General Public
- License</citetitle> as published by the Free Software Foundation;
- either version 2 of the License, or (at your option) any later
- version.
- </para>
- <para>
- This program is distributed in the hope that it will be useful, but
- WITHOUT ANY WARRANTY; without even the implied warranty of
- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- <citetitle>GNU General Public License</citetitle> for more details.
- </para>
- <para>
- A copy of the <citetitle>GNU General Public License</citetitle> is
- included as an appendix to the <citetitle>GNOME Users
- Guide</citetitle>. You may also obtain a copy of the
- <citetitle>GNU General Public License</citetitle> from the Free
- Software Foundation by visiting <ulink type="http"
- url="http://www.fsf.org">their Web site</ulink> or by writing to
- <address>
- Free Software Foundation, Inc.
- <street>59 Temple Place</street> - Suite 330
- <city>Boston</city>, <state>MA</state> <postcode>02111-1307</postcode>
- <country>USA</country>
- </address>
- </para>
- </sect1>
-</article>
-
-<!-- CSC: valid element tags
-<sect1 id="intro"> <title>Introduction</title> ...
-<sect2 id="what"> <title>What is Matita?</title>
-<para>
-<note> <title>Note:</title> <para> ...
-<footnote> <para> ...
-<itemizedlist mark="opencircle">
- <listitem>
- <para>
- The computer player for Iagno is easy to beat.
- </para>
- </listitem>
- </itemizedlist>
-
-<ulink type="http" url="http://www.gnome.org/gdp">
-<email>itp@gnu.org</email>
-<application>Matita</application>
-<command>iagno</command> on the command line
-<citetitle>Othello</citetitle>
-
-<guimenuitem>Iagno</guimenuitem>
-<guisubmenu>Games</guisubmenu>
-<guibutton>none</guibutton>
-<menuchoice> <guimenu>Settings</guimenu> <guisubmenu>Preferences </guisubmenu> </menuchoice>
-
-<xref linkend="start-shot"/>.
-<figure id="start-shot">
- <title>Starting Position</title>
- <screenshot>
- <mediaobject>
- <imageobject>
- <imagedata fileref="figures/START.png" format="PNG" srccredit="Eric Baudais"/>
- </imageobject>
- <textobject>
- <phrase>Screenshot of the starting position.</phrase>
- </textobject>
- </mediaobject>
- </screenshot>
-</figure>
-
--->
projects / helm.git / blobdiff