# HG changeset patch
# User wenzelm
# Date 1468226634 -7200
# Node ID c956d995bec62918c94155b595e414e6df8c04da
# Parent  aa03b0487bf5a6182dd9d72563c65776a9315211
more indentation for quasi_command keywords;

diff -r aa03b0487bf5 -r c956d995bec6 src/HOL/Typedef.thy
--- a/src/HOL/Typedef.thy	Mon Jul 11 10:43:27 2016 +0200
+++ b/src/HOL/Typedef.thy	Mon Jul 11 10:43:54 2016 +0200
@@ -6,7 +6,9 @@
 
 theory Typedef
 imports Set
-keywords "typedef" :: thy_goal and "morphisms"
+keywords
+  "typedef" :: thy_goal and
+  "morphisms" :: quasi_command
 begin
 
 locale type_definition =
diff -r aa03b0487bf5 -r c956d995bec6 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Jul 11 10:43:27 2016 +0200
+++ b/src/Pure/Pure.thy	Mon Jul 11 10:43:54 2016 +0200
@@ -6,13 +6,12 @@
 
 theory Pure
 keywords
-    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>"
-    "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
-    "\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
-    "defines" "rewrites" "fixes" "for" "if" "in" "includes" "infix"
-    "infixl" "infixr" "is" "notes" "obtains" "open" "output"
-    "overloaded" "pervasive" "premises" "private" "qualified" "rewrites"
-    "shows" "structure" "unchecked" "where" "when" "|"
+    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
+    "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
+    "open" "output" "overloaded" "pervasive" "premises" "private" "qualified"
+    "structure" "unchecked" "where" "when" "|"
+  and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites"
+    "obtains" "shows" :: quasi_command
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl == ""
diff -r aa03b0487bf5 -r c956d995bec6 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 10:43:27 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 10:43:54 2016 +0200
@@ -51,10 +51,20 @@
           def head_token(line: Int): Option[Token] =
             nav.iterator(line, 1).toStream.headOption.map(_.info)
 
+          def head_is_quasi_command(line: Int): Boolean =
+            head_token(line) match {
+              case None => false
+              case Some(tok) => keywords.is_quasi_command(tok)
+            }
+
           def prev_command: Option[Token] =
             nav.reverse_iterator(prev_line, 1).
               collectFirst({ case Text.Info(_, tok) if tok.is_command => tok })
 
+          def prev_span: Iterator[Token] =
+            nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_command)
+
+
           def line_indent(line: Int): Int =
             if (line < 0 || line >= buffer.getLineCount) 0
             else buffer.getCurrentIndentForLine(line, null)
@@ -70,6 +80,10 @@
             if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
             else 0
 
+          def indent_extra: Int =
+            if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
+            else 0
+
           def indent_structure: Int =
             nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
               { case ((ind, _), Text.Info(range, tok)) =>
@@ -85,17 +99,25 @@
 
           val indent =
             head_token(current_line) match {
-              case None => indent_structure
+              case None => indent_structure + indent_extra
               case Some(tok) =>
                 if (keywords.is_command(tok, Keyword.theory)) 0
                 else if (tok.is_command) indent_structure - indent_offset(tok)
-                else
+                else {
                   prev_command match {
-                    case None => line_indent(prev_line)
+                    case None =>
+                      val extra =
+                        (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
+                          case (true, true) | (false, false) => 0
+                          case (true, false) => - indent_extra
+                          case (false, true) => indent_extra
+                        }
+                      line_indent(prev_line) + extra
                     case Some(prev_tok) =>
                       indent_structure - indent_offset(prev_tok) -
                       indent_indent(prev_tok) + indent_size
                   }
+               }
             }
 
           actions.clear()