# HG changeset patch # User wenzelm # Date 1541866329 -3600 # Node ID e1d01b351724abcea38497fabf9a2813082497a9 # Parent e6997512ef6cc0611f4094eb142233f43b7b974b more formal references; diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Buffer.hs --- a/src/Tools/Haskell/Buffer.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Buffer.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) Efficient text buffers. + +See also "$ISABELLE_HOME/src/Pure/General/buffer.ML". -} module Isabelle.Buffer (T, empty, add, content) diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/File.hs --- a/src/Tools/Haskell/File.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/File.hs Sat Nov 10 17:12:09 2018 +0100 @@ -4,7 +4,9 @@ Author: Makarius LICENSE: BSD 3-clause (Isabelle) -File-system operations +File-system operations. + +See also "$ISABELLE_HOME/src/Pure/General/file.ML". -} module Isabelle.File (setup, read, write, append) where diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Haskell.thy --- a/src/Tools/Haskell/Haskell.thy Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Haskell.thy Sat Nov 10 17:12:09 2018 +0100 @@ -33,6 +33,8 @@ LICENSE: BSD 3-clause (Isabelle) Basic library of Isabelle idioms. + +See also \<^file>\$ISABELLE_HOME/src/Pure/General/basics.ML\, \<^file>\$ISABELLE_HOME/src/Pure/library.ML\. -} module Isabelle.Library ( @@ -122,6 +124,8 @@ LICENSE: BSD 3-clause (Isabelle) Plain values, represented as string. + +See also \<^file>\$ISABELLE_HOME/src/Pure/General/value.ML\. -} module Isabelle.Value @@ -173,6 +177,8 @@ LICENSE: BSD 3-clause (Isabelle) Efficient text buffers. + +See also \<^file>\$ISABELLE_HOME/src/Pure/General/buffer.ML\. -} module Isabelle.Buffer (T, empty, add, content) @@ -197,6 +203,8 @@ LICENSE: BSD 3-clause (Isabelle) Property lists. + +See also \<^file>\$ISABELLE_HOME/src/Pure/General/properties.ML\. -} module Isabelle.Properties (Entry, T, defined, get, put, remove) @@ -229,6 +237,8 @@ LICENSE: BSD 3-clause (Isabelle) Quasi-abstract markup elements. + +See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/markup.ML\. -} module Isabelle.Markup ( @@ -521,7 +531,9 @@ Author: Makarius LICENSE: BSD 3-clause (Isabelle) -File-system operations +File-system operations. + +See also \<^file>\$ISABELLE_HOME/src/Pure/General/file.ML\. -} module Isabelle.File (setup, read, write, append) where @@ -555,6 +567,8 @@ LICENSE: BSD 3-clause (Isabelle) Untyped XML trees and representation of ML values. + +See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\. -} module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of) @@ -632,6 +646,8 @@ LICENSE: BSD 3-clause (Isabelle) XML as data representation language. + +See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\. -} module Isabelle.XML.Encode ( @@ -716,6 +732,8 @@ LICENSE: BSD 3-clause (Isabelle) XML as data representation language. + +See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/xml.ML\. -} module Isabelle.XML.Decode ( @@ -825,6 +843,8 @@ LICENSE: BSD 3-clause (Isabelle) Generic pretty printing module. + +See also \<^file>\$ISABELLE_HOME/src/Pure/General/pretty.ML\. -} module Isabelle.Pretty ( @@ -978,6 +998,8 @@ Efficient text representation of XML trees. Suitable for direct inlining into plain text. + +See also \<^file>\$ISABELLE_HOME/src/Pure/PIDE/yxml.ML\. -} module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup, @@ -1103,6 +1125,8 @@ LICENSE: BSD 3-clause (Isabelle) Lambda terms, types, sorts. + +See also \<^file>\$ISABELLE_HOME/src/Pure/term.scala\. -} module Isabelle.Term ( @@ -1148,6 +1172,8 @@ LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. + +See also \<^file>\$ISABELLE_HOME/src/Pure/term_xml.ML\. -} {-# LANGUAGE LambdaCase #-} @@ -1188,6 +1214,8 @@ LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. + +See also \<^file>\$ISABELLE_HOME/src/Pure/term_xml.ML\. -} module Isabelle.Term_XML.Decode (sort, typ, term) diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Library.hs --- a/src/Tools/Haskell/Library.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Library.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) Basic library of Isabelle idioms. + +See also "$ISABELLE_HOME/src/Pure/General/basics.ML", "$ISABELLE_HOME/src/Pure/library.ML". -} module Isabelle.Library ( diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Markup.hs --- a/src/Tools/Haskell/Markup.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Markup.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) Quasi-abstract markup elements. + +See also "$ISABELLE_HOME/src/Pure/PIDE/markup.ML". -} module Isabelle.Markup ( diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Pretty.hs --- a/src/Tools/Haskell/Pretty.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Pretty.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) Generic pretty printing module. + +See also "$ISABELLE_HOME/src/Pure/General/pretty.ML". -} module Isabelle.Pretty ( diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Properties.hs --- a/src/Tools/Haskell/Properties.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Properties.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) Property lists. + +See also "$ISABELLE_HOME/src/Pure/General/properties.ML". -} module Isabelle.Properties (Entry, T, defined, get, put, remove) diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Term.hs --- a/src/Tools/Haskell/Term.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Term.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) Lambda terms, types, sorts. + +See also "$ISABELLE_HOME/src/Pure/term.scala". -} module Isabelle.Term ( diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Term_XML/Decode.hs --- a/src/Tools/Haskell/Term_XML/Decode.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Term_XML/Decode.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. + +See also "$ISABELLE_HOME/src/Pure/term_xml.ML". -} module Isabelle.Term_XML.Decode (sort, typ, term) diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Term_XML/Encode.hs --- a/src/Tools/Haskell/Term_XML/Encode.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Term_XML/Encode.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) XML data representation of lambda terms. + +See also "$ISABELLE_HOME/src/Pure/term_xml.ML". -} {-# LANGUAGE LambdaCase #-} diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/Value.hs --- a/src/Tools/Haskell/Value.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/Value.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) Plain values, represented as string. + +See also "$ISABELLE_HOME/src/Pure/General/value.ML". -} module Isabelle.Value diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/XML.hs --- a/src/Tools/Haskell/XML.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/XML.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) Untyped XML trees and representation of ML values. + +See also "$ISABELLE_HOME/src/Pure/PIDE/xml.ML". -} module Isabelle.XML (Attributes, Body, Tree(..), wrap_elem, unwrap_elem, content_of) diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/XML/Decode.hs --- a/src/Tools/Haskell/XML/Decode.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/XML/Decode.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) XML as data representation language. + +See also "$ISABELLE_HOME/src/Pure/PIDE/xml.ML". -} module Isabelle.XML.Decode ( diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/XML/Encode.hs --- a/src/Tools/Haskell/XML/Encode.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/XML/Encode.hs Sat Nov 10 17:12:09 2018 +0100 @@ -5,6 +5,8 @@ LICENSE: BSD 3-clause (Isabelle) XML as data representation language. + +See also "$ISABELLE_HOME/src/Pure/PIDE/xml.ML". -} module Isabelle.XML.Encode ( diff -r e6997512ef6c -r e1d01b351724 src/Tools/Haskell/YXML.hs --- a/src/Tools/Haskell/YXML.hs Sat Nov 10 17:07:17 2018 +0100 +++ b/src/Tools/Haskell/YXML.hs Sat Nov 10 17:12:09 2018 +0100 @@ -6,6 +6,8 @@ Efficient text representation of XML trees. Suitable for direct inlining into plain text. + +See also "$ISABELLE_HOME/src/Pure/PIDE/yxml.ML". -} module Isabelle.YXML (charX, charY, strX, strY, detect, output_markup,