Documentation fixes.

doc/mk_api_doc.py

@@ -226,12 +226,14 @@ try:
     website_dox_substitutions = {}
     bullet_point_prefix='\n   - '
     if Z3PY_ENABLED:
+        print("Python documentation enabled")
         website_dox_substitutions['PYTHON_API'] = (
             '{prefix}<a class="el" href="namespacez3py.html">Python API</a> '
             '(also available in <a class="el" href="z3.html">pydoc format</a>)'
             ).format(
                 prefix=bullet_point_prefix)
     else:
+        print("Python documentation disabled")
         website_dox_substitutions['PYTHON_API'] = ''
     if DOTNET_ENABLED:
         website_dox_substitutions['DOTNET_API'] = (
@@ -250,7 +252,7 @@ try:
         website_dox_substitutions['JAVA_API'] = ''
     if ML_ENABLED:
         website_dox_substitutions['OCAML_API'] = (
-            '<a class="el" href="ml/index.html">ML/OCaml API</a>'
+            '{prefix}<a class="el" href="ml/index.html">ML/OCaml API</a>'
             ).format(
                 prefix=bullet_point_prefix)
     else:
@@ -316,7 +318,7 @@ try:
     if ML_ENABLED:
         ml_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'ml')
         mk_dir(ml_output_dir)
-        if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, doc_path('../src/api/ml/z3enums.mli'), doc_path('../src/api/ml/z3.mli')]) != 0:
+        if subprocess.call(['ocamldoc', '-html', '-d', ml_output_dir, '-sort', '-hide', 'Z3', '-I', '%s/api/ml' % BUILD_DIR, '%s/api/ml/z3enums.mli' % BUILD_DIR, '%s/api/ml/z3.mli' % BUILD_DIR]) != 0:
             print("ERROR: ocamldoc failed.")
             exit(1)
         print("Generated ML/OCaml documentation.")
@@ -326,3 +328,4 @@ except Exception:
     exctype, value = sys.exc_info()[:2]
     print("ERROR: failed to generate documentation: %s" % value)
     exit(1)
+

src/api/ml/z3.mli

@@ -3443,12 +3443,10 @@ sig
 
   (** Parse the given string using the SMT-LIB2 parser.
 
-      {!parse_smtlib_string}
       @return A conjunction of assertions in the scope (up to push/pop) at the end of the string. *)
   val parse_smtlib2_string : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
 
-  (** Parse the given file using the SMT-LIB2 parser.
+  (** Parse the given file using the SMT-LIB2 parser. *)
-      {!parse_smtlib2_string} *)
   val parse_smtlib2_file : context -> string -> Symbol.symbol list -> Sort.sort list -> Symbol.symbol list -> FuncDecl.func_decl list -> Expr.expr
 end
 

src/api/z3_api.h

@@ -1331,7 +1331,7 @@ typedef enum {
    - Z3_IOB:           Index out of bounds.
    - Z3_INVALID_ARG:   Invalid argument was provided.
    - Z3_PARSER_ERROR:  An error occurred when parsing a string or file.
-   - Z3_NO_PARSER:     Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib_string or #Z3_parse_smtlib_file.
+   - Z3_NO_PARSER:     Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib2_string or #Z3_parse_smtlib2_file.
    - Z3_INVALID_PATTERN: Invalid pattern was used to build a quantifier.
    - Z3_MEMOUT_FAIL:   A memory allocation failure was encountered.
    - Z3_FILE_ACCESS_ERRROR: A file could not be accessed.